Let x0 of type ι be given.

Assume H0: 3f728.. x0.

Apply H0 with λ x1 . x1 = 59e44.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (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.

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

Let x3 of type ι → ο be given.

Let x4 of type ι be given.

Assume H2: prim1 x4 x1.

Let x5 of type ι be given.

Assume H3: prim1 x5 x1.

Apply unknownprop_a896d9879197a251fd7a12d69d8f360e5a92ebd292b2039bc93c32a66d0d6a96 with x1, x2, x3, x4, x5, λ x6 x7 . 59e44.. x1 x2 x3 x4 x5 = 59e44.. x6 (e3162.. (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_b2ff742e5629d24773381d0c70489e2e61d08f0a79b04e01904340003f191669 with x1, x2, x3, x4, x5, λ x6 x7 . 59e44.. x1 x2 x3 x4 x5 = 59e44.. x1 (e3162.. (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_cc70c9bfee05595139583a70a5077f4fab54212eeff0ace2bed75137e8c815be with x1, x2, x3, x4, x5, λ x6 x7 . 59e44.. x1 x2 x3 x4 x5 = 59e44.. x1 (e3162.. (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.

Apply unknownprop_156ad6f4abae2729d1934390d4e748ef50cc8fc1690f7498eb2c2ec5f6f593a2 with x1, x2, e3162.. (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, decode_p (f482f.. (59e44.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

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

Let x6 of type ι be given.

Assume H4: prim1 x6 x1.

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

The subproof is completed by applying H4.

The subproof is completed by applying iff_refl with x3 x6.

■

Proofgold Proof