Proofgold Term Root Disambiguation

∀ x0 x1 . x1 ∈ x0 ⟶ x0 = binunion (setminus x0 (Sing x1)) (Sing x1)

as obj
-

as prop
eb0c4..^{binunion_remove1_eq}

theory
HotG

stx
594e8..

address
TMFKV..^{binunion_remove1_eq}