Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ add_SNo x3 x1 = add_SNo x1 x3) ⟶ SNo x2 ⟶ x2 ∈ SNoS_ (SNoLev x0) ⟶ add_SNo x2 x1 = add_SNo x1 x2

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_SNo_com__2__3

proofgold address
TMQ3d..^{Conj_add_SNo_com__2__3}

creator
35053 PrNpY../143fb..

owner
35061 PrNpY../16921..

term root
26f46..