Proofgold Proposition

∀ x0 . SNo x0 ⟶ ∀ x1 x2 . SNoCutP x1 x2 ⟶ x0 = SNoCut x1 x2 ⟶ minus_SNo x0 = SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)

type
prop

theory
HotG

name
minus_SNoCut_eq_lem

proof
PUK1b..

Megalodon
minus_SNoCut_eq_lem

proofgold address
TMRBu..^{minus_SNoCut_eq_lem}

creator
4949 Pr6Pc../97c99..

owner
4949 Pr6Pc../97c99..

term root
29069..