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 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_b8b34a52999e886cc19aacd0dfc98c11cacae87a6c6875441ad2cdcc84e15f13 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
f482f.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
decode_p (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_0584a84ffb1c701f11568ad09c12208aa203b83beb664047f3b41e307f006380 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_7406e4b4e96091f751b5e3e732abecdf4c8b326895755f8fbe97e4e3b9a7c699 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_6fe4748b552c1cdd2fd9e34a6e95c32a6e059b0f8c1228e79280b405dc1c3efd with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Apply unknownprop_ae503b83ae9d7f088146b2bb572620ee5684172e580f4c67c9abf2d4251cf16f with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x5 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x5 x6.