Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Apply ordinal_ind with
λ x2 . or (∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3) (∃ x3 . and (prim1 x3 x2) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4)).
Let x2 of type ι be given.
Apply H2 with
(∀ x3 . prim1 x3 x2 ⟶ or (∃ x4 : ι → ο . 078b6.. x0 x1 x3 x4) (∃ x4 . and (prim1 x4 x3) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5))) ⟶ or (∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3) (∃ x3 . and (prim1 x3 x2) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4)).
Apply dneg with
or (∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3) (∃ x3 . and (prim1 x3 x2) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4)).
Apply not_or_and_demorgan with
∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3,
∃ x3 . and (prim1 x3 x2) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4),
False leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7:
not (∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3).
Apply unknownprop_63cf8167ec21b344b97624441aeddfcf366466436f5a81c6bd27f9ec03224f29 with
x2,
False leaving 3 subgoals.
The subproof is completed by applying H2.
Apply H7.
Let x3 of type ο be given.
Assume H13:
∀ x4 : ι → ο . 078b6.. x0 x1 x2 x4 ⟶ x3.
Apply H13 with
λ x4 . ∀ x5 : ι → ο . 8033b.. x0 x1 (4ae4a.. x4) x5 ⟶ x5 x4.