Proofgold Term Root Disambiguation

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 x5 . SNoCutP x4 x5 ⟶ x3 = SNoCut x4 x5 ⟶ minus_SNo x3 = SNoCut (prim5 x5 minus_SNo) (prim5 x4 minus_SNo)) ⟶ SNoCutP x1 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ SNo x3) ⟶ x0 = SNoCut x1 x2 ⟶ SNo (SNoCut x1 x2) ⟶ minus_SNo x0 = SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)

as obj
-

as prop
9d1d7..^{Conj_minus_SNoCut_eq_lem__11__3}

theory
HotG

stx
b740c..

address
TMEtu..^{Conj_minus_SNoCut_eq_lem__11__3}