Proofgold Term Root Disambiguation

∀ x0 . Unj (Inj0 x0) = x0

as obj
-

as prop
3808a..^Unj_Inj0_eq

theory
HotG

stx
114a5..

address
TMZUK..^Unj_Inj0_eq