Proofgold Term Root Disambiguation

∀ x0 x1 . Sing x0 = x1 ⟶ and (x0 ∈ x1) (∀ x2 . x2 ∈ x1 ⟶ x2 = x0)

as obj
-

as prop
199c6..^Sing_inv

theory
HotG

stx
91633..

address
TMGqo..^Sing_inv