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 ⟶ SNoCutP (prim5 x2 minus_SNo) (prim5 x1 minus_SNo) ⟶ SNo (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)) ⟶ (∀ x3 . SNo x3 ⟶ (∀ x4 . x4 ∈ prim5 x2 minus_SNo ⟶ SNoLt x4 x3) ⟶ (∀ x4 . x4 ∈ prim5 x1 minus_SNo ⟶ SNoLt x3 x4) ⟶ and (SNoLev (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo))) (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)) x3)) ⟶ (∀ x3 . x3 ∈ prim5 x2 minus_SNo ⟶ SNoLt x3 (minus_SNo x0)) ⟶ (∀ x3 . x3 ∈ prim5 x1 minus_SNo ⟶ SNoLt (minus_SNo x0) x3) ⟶ minus_SNo x0 = SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)

as obj
-

as prop
da648..^{Conj_minus_SNoCut_eq_lem__8__3}

theory
HotG

stx
b740c..

address
TMQiV..^{Conj_minus_SNoCut_eq_lem__8__3}