Let x0 of type ι be given.

Assume H0: 56056.. x0.

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

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_4446df303565862bba749bc3b3796f1833a33e7c7081a067192379a7c1d64c04 with x1, x2, x3, x4, x5, λ x6 x7 . 98165.. x1 x2 x3 x4 x5 = 98165.. x6 (decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_f69656ed661027e20424f9892bdd76c006ab20fc5d7ad4c2ac380a23f2b07cf7 with x1, x2, x3, x4, x5, λ x6 x7 . 98165.. x1 x2 x3 x4 x5 = 98165.. x1 (decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_12482a7f3b6d06d949ae831c83e57b0424853f81e2459db4981aead803933efa with x1, x2, x3, x4, x5, λ x6 x7 . 98165.. x1 x2 x3 x4 x5 = 98165.. x1 (decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.

Apply unknownprop_beb7665a02494ecb3c990dfb1fc53983a537b07e86e5d1431527bdfa7158f594 with x1, x2, decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, decode_p (f482f.. (98165.. 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_942aa5d8b4e5ee282c21621bfe762ed5c1586eafb0f3bffa1e4e44c94b9c7e56 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.

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

The subproof is completed by applying H3.

The subproof is completed by applying iff_refl with x3 x6.

■

Proofgold Proof