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.
Assume H0:
∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x4 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4.
Apply unknownprop_a6aeec7577d8b45f51a1b4fa07acbb2f80ce2cce3db0917ad7941ddc11875166 with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (decode_c (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
decode_c (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
Let x5 of type ι → ο be given.
Assume H1:
∀ x6 . x5 x6 ⟶ prim1 x6 x1.
Apply unknownprop_d0c017880678fcd65ad99be7e828cd3a18ab65c5cb6e8cacc01cf0609a657630 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 : ο . iff (x2 x5) x6 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x2 x5.
The subproof is completed by applying unknownprop_ceb24fa1059e011557ca4438b2dcc412c46fba0e11220c6e3b75388ad54ca8ce with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_8cc962999b2979b6bcbb6e4634188c09a486b85cbb8d9eb0200122c4937499d8 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x4 x5 x6) x7 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 x5 x6.