Proofgold Term Root Disambiguation

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

as obj
77512..^SNoCutP

as prop
-

theory
HotG

stx
fab7c..

address
TMdYB..^SNoCutP