Proofgold Term Root Disambiguation

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

as obj
0e9f0..^SNo_max_of

as prop
-

theory
HotG

stx
5128f..

address
TMQxZ..^SNo_max_of