Proofgold Term Root Disambiguation

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

as obj
-

as prop
11eb0..^{minus_SNoCut_eq_lem}

theory
HotG

stx
2cf07..

address
TMJJo..^{minus_SNoCut_eq_lem}