Proofgold Term Root Disambiguation

∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 (λ x3 . In x3 x1) (λ x3 . In x3 x2)

as obj
-

as prop
f2976..^SNoEq_E

theory
HF

stx
8964b..

address
TMGkp..^SNoEq_E