set y0 to be ...
set y1 to be ...
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with
∃ x2 . and (∀ x3 . y0 x3 ⟶ ∀ x4 . In x4 x2 ⟶ ∀ x5 . Subq x5 x4 ⟶ ∀ x6 . ordinal (SNoLev x5)) (∀ x3 . and (∃ x4 . and (y1 x3 x4) (not (exactly5 x3))) (exactly5 x3) ⟶ ∀ x4 . In x4 (binrep (Power (Power (Power (Power 0)))) (Power (Power 0))) ⟶ ∃ x5 . and (Subq x5 x2) (∃ x6 . and (Subq x6 x5) (exactly5 x6))).
set y2 to be ...
set y3 to be ...
set y4 to be ...
set y5 to be ...
set y6 to be ...
set y7 to be ...
Apply notE with
exactly5 (Eps_i (y4 y1 0)) leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
exactly5 (Eps_i (y4 y1 0)).
Apply notE with
In (Eps_i (y2 0)) 0 leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
In (Eps_i (y2 0)) 0.
The subproof is completed by applying H8.
Apply notE with
In (Eps_i (y2 0)) 0 leaving 2 subgoals.
Apply unknownprop_e71e48a383f529f68afdc14358189461de3d3a97993b62a8cb1f5e89e6531b39 with
λ x8 . In x8 0,
Eps_i (y2 0).
The subproof is completed by applying unknownprop_641980b1f679699e58af9b75e8660e324a5a8b56d6549ff9c993636d65c0d9dc.
The subproof is completed by applying L9.
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with
In (Eps_i (y2 0)) 0.
Apply notE with
not (In (Eps_i (y2 0)) 0) leaving 2 subgoals.
Apply unknownprop_b6f324b8b8816479c1306f727dc14fcaec89d74751f4c27e6f83110cd1b0b495 with
In (Eps_i (y2 0)) 0.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with
In (Eps_i (y2 0)) 0,
not (∀ x8 . Subq x8 (Eps_i (y2 0)) ⟶ ∀ x9 . ordinal (SNoLev x8)).
Apply unknownprop_f900d1a90bf5d347b18522211f82fb33d0afc1127e77502891326c698226d151 with
In (Eps_i (y2 0)) 0,
∀ x8 . Subq x8 (Eps_i (y2 0)) ⟶ ∀ x9 . ordinal (SNoLev x8).
set y8 to be ...
set y9 to be ...
Apply L15 with
λ x10 x11 : ι → ι → ο . y9 x10,
λ x10 x11 : ι → ο . y9 x10 leaving 3 subgoals.
Let x10 of type (ι → ο) → (ι → ο) → ο be given.
Assume H22: x10 (y3 0) (y3 0).
The subproof is completed by applying H22.
The subproof is completed by applying Eps_i_ex with y4 0.
Apply unknownprop_8b701add31660a0d5e89a46b82b6ff470102e24ed0b9b8e48634f33a4b4aaf64 with
λ x10 . In x10 0 ⟶ ∀ x11 . Subq x11 x10 ⟶ ∀ x12 . ordinal (SNoLev x11).
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with
y2 (Eps_i (y8 y2 0)),
not (∀ x10 . ... ⟶ ∀ x11 . Subq x11 ... ⟶ ∀ x12 . ordinal (SNoLev x11)).