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 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_96e325f5225007f883608ced691e198c9132e00df04ef6b043937abf9b283533 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_e5de091bc243fc8af09a52f41bd7457d930b22a1ee185a483ac9d233b589104d with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_64e46c7a48eac1f7008652d9ab91808a3afbbfe70ec8208c5ad3733a08258cf5 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_41bee463d2b841a1f67904f27e4108ff00fd68bb9c970dddc779208040bf4303 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.
Let x7 of type ι be given.
Apply unknownprop_2ef8d35badf747d6423713318afe09404bd82f4166069eb04b62dba2a480a3f4 with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x5 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 x5 x6 x7.