Let x0 of type ι → (ι → ι) → (ι → ο) → ι → ι → ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι be given.

Let x3 of type ι → ο be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H0: ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.

Apply unknownprop_f765175e49be2e5a6aa2dddd3f196b09de0d3db9e2abfd3e4e13e6768629fafe with x1, x2, x3, x4, x5, λ x6 x7 . x0 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..))))) = x0 x1 x2 x3 x4 x5.

Apply unknownprop_dcbb4c59274350f3f1d7187419c84249f504e8939c586146795768afcc9fb03f with x1, x2, x3, x4, x5, λ x6 x7 . x0 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..))))) = x0 x1 x2 x3 x4 x5.

Apply unknownprop_2dccef3492650341a1b94804dbaa3d10f6307d1141b055c4c1e8d5afc270c4ed with x1, x2, x3, x4, x5, λ x6 x7 . x0 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 = x0 x1 x2 x3 x4 x5.

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

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

Let x6 of type ι be given.

Assume H1: 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 H1.

The subproof is completed by applying iff_refl with x3 x6.

■

Proofgold Proof