Proofgold Term Root Disambiguation

wceq cid (copab (λ x0 x1 . wceq (cv x0) (cv x1)))

as obj
-

as prop
614d8..

theory
SetMM

stx
e4700..

address
TMK5Z..