set y0 to be ...
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with
(∃ x1 . and (In x1 0) (∀ x2 . (∀ x3 . Subq x3 x1 ⟶ and (∃ x4 . and (In x4 x2) (∃ x5 . and (nat_p x4) (not (TransSet x1)))) (∃ x4 . and (∃ x5 . and (not (atleast3 0)) (not (atleast3 (binrep (Power (Power (Power (Power 0)))) (Power (Power 0)))))) (and (exactly2 x1) (∀ x5 . Subq x5 x1 ⟶ and (not (TransSet x2)) (In x5 x3)))) ⟶ ∀ x4 . In x4 x2 ⟶ (∃ x5 . and (Subq x5 x4) (TransSet x1)) ⟶ not (atleast5 x4)) ⟶ ∀ x3 . atleast4 (Power (Power (Power (Power 0)))))) ⟶ y0.
set y1 to be ...
Apply notE with
In (Eps_i y1) 0 leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
In (Eps_i y1) 0.
The subproof is completed by applying H2.
Apply notE with
In (Eps_i y1) 0 leaving 2 subgoals.
Apply unknownprop_e71e48a383f529f68afdc14358189461de3d3a97993b62a8cb1f5e89e6531b39 with
λ x2 . In x2 0,
Eps_i y1.
The subproof is completed by applying unknownprop_641980b1f679699e58af9b75e8660e324a5a8b56d6549ff9c993636d65c0d9dc.
The subproof is completed by applying L3.