Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoCutP (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0)))

type
prop

theory
HotG

name
add_SNo_SNoCutP

proof
PUi5E..

Megalodon
add_SNo_SNoCutP

proofgold address
TMR6c..^{add_SNo_SNoCutP}

creator
4962 Pr6Pc../aa4ca..

owner
4962 Pr6Pc../aa4ca..

term root
e2b7d..