Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ο . binunion (Sep x0 x1) {SetAdjoin x2 (Sing 1)|x2 ∈ x0,not (x1 x2)}

as obj
0a835..^PSNo

as prop
-

theory
HotG

stx
fab7c..

address
TMYCs..^PSNo