Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cmnd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wrex (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cv x2)) (cv x4)) (wceq (co (cv x4) (cv x3) (cv x2)) (cv x4))) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . csgrp))
as obj
-
as prop
e6c37..
theory
SetMM
stx
1a7d4..
address
TMR7f..