Proofgold Term Root Disambiguation

∀ x0 . Unj (Inj0 x0) = x0

as obj
-

as prop
c3d4f..^Unj_Inj0_eq

theory
HF

stx
a6670..

address
TMSwV..^Unj_Inj0_eq