Proofgold Term Root Disambiguation

wceq crrx (cmpt (λ x0 . cvv) (λ x0 . cfv (co crefld (cv x0) cfrlm) ctch))

as obj
-

as prop
aa645..

theory
SetMM

stx
29ebb..

address
TMU9P..