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 ⟶ ∀ x10 . prim1 x10 x1 ⟶ x4 x9 x10 = x8 x9 x10) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_996291121317bd28c520c8830689109eaa5eb658691dbcb92ca5dc25aa0668cb with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
decode_p (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_fc264994e9fe69947f39a2155e3b678222607a73685180f878ae6bee13d7c92e with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f06030f48dfa8b9a3ae3b2086298a361c60007f8d582114218ce4d0e9b3c2f15 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_37557e7f0ffd09d385c71300094cf77a808eb546d116f78961140ab099ada3d4 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Apply unknownprop_afe428c5c12956c8dfb4d90a681589485dc1dc57c1822e0cb3a9b977019fa9eb 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.