Proofgold Term Root Disambiguation

λ x0 x1 . and (and (x1 ∈ x0) (SNo x1)) (∀ x2 . x2 ∈ x0 ⟶ SNo x2 ⟶ SNoLe x1 x2)

as obj
14494..^SNo_min_of

as prop
-

theory
HotG

stx
5128f..

address
TMSNf..^SNo_min_of