Proofgold Term Root Disambiguation

∀ x0 x1 x2 . (∀ x3 . prim1 x3 x0 ⟶ iff (prim1 x3 x1) (prim1 x3 x2)) ⟶ SNoEq_ x0 x1 x2

as obj
-

as prop
9239a..

theory
HoTg

stx
38a69..

address
TMaox..^SNoEq_I