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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_0cf25aee1aa3da57541ced65711a31bdf8c1adc2842aaacec0283988f600ba28 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (decode_c (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_94d5d45a49954094229a693debff9e0992350d175dfdfc61f9a83c91eb555ae2 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_efd5b0e4635a13150619341727a4e9f3237b474d633dc1b7cfc9d6140575d9f7 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
decode_c (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
2b2e3.. (f482f.. (fe7e3.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
Let x6 of type ι → ο be given.
Assume H1:
∀ x7 . x6 x7 ⟶ prim1 x7 x1.
Apply unknownprop_bd7df01b1bb51569937528679c59d4ba358b10f67a8c2200468ec7fa888fb726 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.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_b3896936979d3dfc36b30b98f712f7e9af8a0e1fec901b0aa1270247d172a448 with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x3 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 x3 x6 x7.