Proofgold Term Root Disambiguation

wceq cgr (cab (λ x0 . wex (λ x1 . w3a (wf (cxp (cv x1) (cv x1)) (cv x1) (cv x0)) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x0)) (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x0))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)) (wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x0)) (cv x3)) (wrex (λ x4 . wceq (co (cv x4) (cv x3) (cv x0)) (cv x2)) (λ x4 . cv x1))) (λ x3 . cv x1)) (λ x2 . cv x1)))))

as obj
-

as prop
19765..

theory
SetMM

stx
d4238..

address
TMZiD..