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 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x4 x8 = x7 x8) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4.
Apply unknownprop_f9841c5700593e0ef50430c91cebfc814e6f72caa8c201d852b6621444f2ed27 with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (decode_c (f482f.. (21805.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (21805.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (21805.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
decode_c (f482f.. (21805.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (21805.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
f482f.. (f482f.. (21805.. 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_c9eab367a4df9a853de0437d4227e12fb7dd1c1608fea8e3b9c94688d5a7f039 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_e6864ca128ecf246b5eea16161b87f95b11bea6e378a11a230b13980009ec27d with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_3a77e63fb2543c175ca7597d44850dbb7f8ad75c88f28d45299dc61577d41190 with x1, x2, x3, x4.