Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cgf (cmpt2 (λ x0 x1 . cprime) (λ x0 x1 . cn) (λ x0 x1 . csb (cfv (cv x0) czn) (λ x2 . cfv (co (cv x2) (csn (csb (cfv (cv x2) cpl1) (λ x3 . csb (cfv (cv x2) cv1) (λ x4 . co (co (co (cv x0) (cv x1) cexp) (cv x4) (cfv (cfv (cv x3) cmgp) cmg)) (cv x4) (cfv (cv x3) csg))))) csf) c1st)))
as obj
-
as prop
e06de..
theory
SetMM
stx
a24a7..
address
TMXtj..