Proofgold Term Root Disambiguation

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

as obj
-

as prop
fcab6..^SNoEq_I

theory
HF

stx
8964b..

address
TMJYY..^SNoEq_I