Let x0 of type ι be given.

Assume H0: 781e8.. x0.

Apply H0 with λ x1 . x1 = fe7e3.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (2b2e3.. (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.

Let x4 of type ι be given.

Assume H1: prim1 x4 x1.

Let x5 of type ι be given.

Assume H2: prim1 x5 x1.

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

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

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

Apply unknownprop_58cc1b036a5f8e0124ef530840565bff39734c840f8f3d38d1b426bab04b29fb with x1, x2, decode_c (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, 2b2e3.. (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

Let x6 of type ι → ο be given.

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

Apply unknownprop_bd7df01b1bb51569937528679c59d4ba358b10f67a8c2200468ec7fa888fb726 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.

Let x6 of type ι be given.

Assume H3: prim1 x6 x1.

Let x7 of type ι be given.

Assume H4: prim1 x7 x1.

Apply unknownprop_b3896936979d3dfc36b30b98f712f7e9af8a0e1fec901b0aa1270247d172a448 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x3 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 x3 x6 x7.

■

Proofgold Proof