Proofgold Term Root Disambiguation

∀ x0 x1 . Sing x0 = Sing x1 ⟶ x0 = x1

as obj
-

as prop
96eb7..^Sing_inj

theory
HotG

stx
2a9bf..

address
TMKxv..^Sing_inj