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 : ι → ο . (∀ x8 . x7 x8 ⟶ prim1 x8 x1) ⟶ iff (x2 x7) (x6 x7)) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_a6d0836629b06c347d81c7da0e781e137dc096b4d766909eecd88c641c2406ee with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (decode_c (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
decode_c (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
2b2e3.. (f482f.. (34992.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
Let x6 of type ι → ο be given.
Assume H1:
∀ x7 . x6 x7 ⟶ prim1 x7 x1.
Apply unknownprop_defbe3747f1097ec086fdbeec5d1f2fd8c4d5aac8054b0054e662dc7ed68453e with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x2 x6.
The subproof is completed by applying unknownprop_96b84b0b3cf369c1cec77c41d8595ba2cfdaf06b1d4e4ffc1ca00aae7d7b665d with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_ec3a8c70c3cdb58e6e9eecf0af1ff127cd7d0203cd47b0c8c5d1796ef1bb9b7c with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x4 x6 x7.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_7c9c98220ee1a5fcadfc46c1dd049eefb03d9151de907339a5f75e511f461f65 with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x5 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x5 x6 x7.