Let x0 of type ι be given.

Assume H0: ab832.. x0.

Apply H0 with λ x1 . x1 = bebf6.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Let x1 of type ι be given.

Let x2 of type (ι → ο) → ο be given.

Let x3 of type ι → ι → ι be given.

Assume H1: ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (x3 x4 x5) x1.

Let x4 of type ι → ο be given.

Let x5 of type ι be given.

Assume H2: prim1 x5 x1.

Apply unknownprop_65cce1600a86bdb4fcc47c3f21cd540289b2d8a67dba9d2cfdb16c7b60cd3592 with x1, x2, x3, x4, x5, λ x6 x7 . bebf6.. x1 x2 x3 x4 x5 = bebf6.. x6 (decode_c (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_d541830b9bb76016fdfd9d4a39b99cfc03581aed7733587f376a6613a3d27e18 with x1, x2, x3, x4, x5, λ x6 x7 . bebf6.. x1 x2 x3 x4 x5 = bebf6.. x1 (decode_c (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6.

Apply unknownprop_651be5e42e9dbaeea44e71f64347019584d1d8cd23092d631b3bc64b94525999 with x1, x2, decode_c (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, decode_p (f482f.. (bebf6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5 leaving 3 subgoals.

Let x6 of type ι → ο be given.

Assume H3: ∀ x7 . x6 x7 ⟶ prim1 x7 x1.

Apply unknownprop_893520f3075c4d3a8ba22723b37a813951891a352483f9ee1c79192185721ed8 with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying iff_refl with x2 x6.

The subproof is completed by applying unknownprop_d00271e3409a7f60fd60ced864a095054ad7fb1dd9954a22fb8f485fbf2f84a4 with x1, x2, x3, x4, x5.

Let x6 of type ι be given.

Assume H3: prim1 x6 x1.

Apply unknownprop_8472672de8e4a6002250f4bca01a91b0df686dd5f362cb55afa19360ce15f05d with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x4 x6) x7 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying iff_refl with x4 x6.

■

Proofgold Proof