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

Let x1 of type ι be given.

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

Let x3 of type ι → ο be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H0: ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.

Apply unknownprop_a896d9879197a251fd7a12d69d8f360e5a92ebd292b2039bc93c32a66d0d6a96 with x1, x2, x3, x4, x5, λ x6 x7 . x0 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..))))) = x0 x1 x2 x3 x4 x5.

Apply unknownprop_b2ff742e5629d24773381d0c70489e2e61d08f0a79b04e01904340003f191669 with x1, x2, x3, x4, x5, λ x6 x7 . x0 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..))))) = x0 x1 x2 x3 x4 x5.

Apply unknownprop_cc70c9bfee05595139583a70a5077f4fab54212eeff0ace2bed75137e8c815be with x1, x2, x3, x4, x5, λ x6 x7 . x0 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 = x0 x1 x2 x3 x4 x5.

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

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

Let x6 of type ι be given.

Assume H1: 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 H1.

The subproof is completed by applying iff_refl with x3 x6.

■

Proofgold Proof