Proofgold Term Root Disambiguation

∀ x0 . Inj1 x0 = binunion (Sing 0) (prim5 x0 Inj1)

as obj
-

as prop
b8045..^Inj1_eq

theory
HotG

stx
114a5..

address
TMVWd..^Inj1_eq