Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq clsh (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wne (cv x1) (cfv (cv x0) cbs)) (wrex (λ x2 . wceq (cfv (cun (cv x1) (csn (cv x2))) (cfv (cv x0) clspn)) (cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs))) (λ x1 . cfv (cv x0) clss)))
as obj
-
as prop
1fbd0..
theory
SetMM
stx
b3a68..
address
TMagu..