Proofgold Term Root Disambiguation

wceq cvc (copab (λ x0 x1 . w3a (wcel (cv x0) cablo) (wf (cxp cc (crn (cv x0))) (crn (cv x0)) (cv x1)) (wral (λ x2 . wa (wceq (co c1 (cv x2) (cv x1)) (cv x2)) (wral (λ x3 . wa (wral (λ x4 . wceq (co (cv x3) (co (cv x2) (cv x4) (cv x0)) (cv x1)) (co (co (cv x3) (cv x2) (cv x1)) (co (cv x3) (cv x4) (cv x1)) (cv x0))) (λ x4 . crn (cv x0))) (wral (λ x4 . wa (wceq (co (co (cv x3) (cv x4) caddc) (cv x2) (cv x1)) (co (co (cv x3) (cv x2) (cv x1)) (co (cv x4) (cv x2) (cv x1)) (cv x0))) (wceq (co (co (cv x3) (cv x4) cmul) (cv x2) (cv x1)) (co (cv x3) (co (cv x4) (cv x2) (cv x1)) (cv x1)))) (λ x4 . cc))) (λ x3 . cc))) (λ x2 . crn (cv x0)))))

as obj
-

as prop
78de4..

theory
SetMM

stx
d4238..

address
TMUky..