Let x0 of type ι be given.

Assume H0: 8b540.. x0.

Apply H0 with λ x1 . x1 = 6b0a5.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (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.

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.

Assume H2: prim1 x4 x1.

Let x5 of type ι be given.

Assume H3: prim1 x5 x1.

Apply unknownprop_60e1285d2ccc72f95127634d66da7efc514376e8511cd196b24e4fbf48de2cda with x1, x2, x3, x4, x5, λ x6 x7 . 6b0a5.. x1 x2 x3 x4 x5 = 6b0a5.. x6 (decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_389229da3772dfd44420288246db584f2385b5b60e9aee278525a0368b3d540c with x1, x2, x3, x4, x5, λ x6 x7 . 6b0a5.. x1 x2 x3 x4 x5 = 6b0a5.. x1 (decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_53e6d529605a4b5256fb5566fea600c12c5ce5c0a664882744edcf0b0e34ad81 with x1, x2, x3, x4, x5, λ x6 x7 . 6b0a5.. x1 x2 x3 x4 x5 = 6b0a5.. x1 (decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.

Apply unknownprop_e6177a62e28b97ff1cc08513edeec685f6dafee1478ff0c3d8cb25879ae1f611 with x1, x2, decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

Let x6 of type ι → ο be given.

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

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

The subproof is completed by applying H4.

The subproof is completed by applying iff_refl with x2 x6.

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

■

Proofgold Proof