Proofgold Term Root Disambiguation

∀ x0 . Unj (Inj1 x0) = x0

as obj
-

as prop
ae00e..^Unj_Inj1_eq

theory
HotG

stx
114a5..

address
TMRKw..^Unj_Inj1_eq