Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo_min_of (SNoR x0) x1 ⟶ ∀ x2 . SNo x2 ⟶ SNoLt x2 x0 ⟶ SNoLt (add_SNo x0 x0) (add_SNo x1 x2) ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ SNoL x2) (add_SNo x1 x4 = add_SNo x0 x0) ⟶ x3) ⟶ x3

as obj
-

as prop
084f0..^{double_SNo_min_1}

theory
HotG

stx
5128f..

address
TMYCQ..^{double_SNo_min_1}