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)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_9c00f8a6468cbf26c7aa2fedf6b7ba6c24299a59bc94ead9a21a4122dc16f1bf with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (f482f.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_e58b74dbd4f3e13e2978ca5351e448c7d44f0c599ffbc5b020aac1e953a0f879 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (f482f.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
f482f.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (2cece.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_c437c083995ca4c7d24f794797f46eebcc8e35fd673d72fa52431b29b930e70f with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_48073b86f4b74bfcd3316dc47dc2e744f1fc1f2567c61579b27dbc9468d39401 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_64ae2dc1960077d9e9f005b67cd30a8fa340c12fc7ca4dacd26c87457b1d6adf 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.