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 ⟶ 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 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_9b935f184e6ef19fd2887b24efdd6195f442b8ceca35e964096d01e16d81456d with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
decode_p (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_33b004c8f62843bcba581c3bb62c1b6860ed0922825af08a3ae7ea18e3233657 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_cc298fd33dfe686ee7b576905469258d62cae8b4852e26a02f0aa0c50d1f2c8b with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_4d5576adce78b831f45c33ebbe5605fa8b4e2b873b249b058e32db9cb78c1ede 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.
Apply unknownprop_83e4e93ebfb84f8cd49bab263850d2028f52dcb8263fa261f8e447c5e6ace519 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.