Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq chos (cmpt2 (λ x0 x1 . co chil chil cmap) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cva)))
as obj
-
as prop
b4143..
theory
SetMM
stx
337cc..
address
TMah6..