Proofgold Term Root Disambiguation

∀ x0 . Unj (Inj1 x0) = x0

as obj
-

as prop
c76aa..^Unj_Inj1_eq

theory
HF

stx
a6670..

address
TMcPq..^Unj_Inj1_eq