Proofgold Proposition

∀ x0 . SNo x0 ⟶ ∀ x1 . SNo x1 ⟶ add_SNo x0 x1 = SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x3 x1|x3 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0)))

type
prop

theory
HotG

name
add_SNo_eq

proof
PUK1b..

Megalodon
add_SNo_eq

proofgold address
TMGPP..^add_SNo_eq

creator
4949 Pr6Pc../f8eff..

owner
4949 Pr6Pc../f8eff..

term root
0c112..