Proofgold Proposition

∀ x0 . SNo_ omega x0 ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ or (and (nIn (SNoLev x1) x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ x2 ∈ x0)) (and (SNoLev x1 ∈ x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ nIn x2 x0))

type
prop

theory
HotG

name
-

proof
PUaSr..

Megalodon
-

proofgold address
TMFWu..

creator
23745 Pr5Zc../eb4ff..

owner
23745 Pr5Zc../eb4ff..

term root
17925..