Let x0 of type ι be given.

Assume H0: 3bcdb.. x0.

Apply H0 with λ x1 . x1 = 04077.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (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_94ece11139b8209a2e93daf4c612a0b513bf60947b0a11709e66c0ffb84c8f1b with x1, x2, x3, x4, x5, λ x6 x7 . 04077.. x1 x2 x3 x4 x5 = 04077.. x6 (decode_c (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_c448475578ebfac6f6cb9c88e3417ee1e70958c3c1396a302801418026fc39aa with x1, x2, x3, x4, x5, λ x6 x7 . 04077.. x1 x2 x3 x4 x5 = 04077.. x1 (decode_c (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6.

Apply unknownprop_1031c22d9fda2870d527411f8e17b533d4d0d47f974620f8768e595bd625cb89 with x1, x2, decode_c (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (04077.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (04077.. 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_4055ab75c251cb089ef299f7053c7b06b3ecf1f8e9ceadb345e463a982d44135 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_f908702b2b458938d6b90a591e3f16c070534310fb46e13c038f9d7cd61e56a9 with x1, x2, x3, x4, x5.

Let x6 of type ι be given.

Assume H3: prim1 x6 x1.

Let x7 of type ι be given.

Assume H4: prim1 x7 x1.

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

The subproof is completed by applying H3.

The subproof is completed by applying H4.

The subproof is completed by applying iff_refl with x4 x6 x7.

■

Proofgold Proof