Let x0 of type ι be given.

Assume H0: 45c1b.. x0.

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

Assume H1: ∀ x3 . prim1 x3 x1 ⟶ prim1 (x2 x3) x1.

Let x3 of type ι → ο be given.

Let x4 of type ι be given.

Assume H2: prim1 x4 x1.

Let x5 of type ι be given.

Assume H3: prim1 x5 x1.

Apply unknownprop_f765175e49be2e5a6aa2dddd3f196b09de0d3db9e2abfd3e4e13e6768629fafe with x1, x2, x3, x4, x5, λ x6 x7 . 726e4.. x1 x2 x3 x4 x5 = 726e4.. x6 (f482f.. (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_dcbb4c59274350f3f1d7187419c84249f504e8939c586146795768afcc9fb03f with x1, x2, x3, x4, x5, λ x6 x7 . 726e4.. x1 x2 x3 x4 x5 = 726e4.. x1 (f482f.. (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_2dccef3492650341a1b94804dbaa3d10f6307d1141b055c4c1e8d5afc270c4ed with x1, x2, x3, x4, x5, λ x6 x7 . 726e4.. x1 x2 x3 x4 x5 = 726e4.. x1 (f482f.. (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.

Apply unknownprop_c97de0ea6508e3b1440ba7011aec54bcc7110d6f0bb44fe80a11fed8f2370250 with x1, x2, f482f.. (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, decode_p (f482f.. (726e4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

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

Let x6 of type ι be given.

Assume H4: prim1 x6 x1.

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

The subproof is completed by applying H4.

The subproof is completed by applying iff_refl with x3 x6.

■

Proofgold Proof