Search for blocks/addresses/...

Proofgold Proposition

wceq cful (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . copab (λ x2 x3 . wa (wbr (cv x2) (cv x3) (co (cv x0) (cv x1) cfunc)) (wral (λ x4 . wral (λ x5 . wceq (crn (co (cv x4) (cv x5) (cv x3))) (co (cfv (cv x4) (cv x2)) (cfv (cv x5) (cv x2)) (cfv (cv x1) chom))) (λ x5 . cfv (cv x0) cbs)) (λ x4 . cfv (cv x0) cbs)))))
type
prop
theory
SetMM
name
df_full
proof
PULi1..
Megalodon
-
proofgold address
TMP6L..
creator
36376 PrCmT../a475d..
owner
36376 PrCmT../a475d..
term root
cb369..