Search for blocks/addresses/...

Proofgold Proposition

wceq cply (cmpt (λ x0 . cpw cc) (λ x0 . cab (λ x1 . wrex (λ x2 . wrex (λ x3 . wceq (cv x1) (cmpt (λ x4 . cc) (λ x4 . csu (co cc0 (cv x2) cfz) (λ x5 . co (cfv (cv x5) (cv x3)) (co (cv x4) (cv x5) cexp) cmul)))) (λ x3 . co (cun (cv x0) (csn cc0)) cn0 cmap)) (λ x2 . cn0))))
type
prop
theory
SetMM
name
df_ply
proof
PUhRH..
Megalodon
-
proofgold address
TMMNQ..
creator
36386 PrCmT../97510..
owner
36386 PrCmT../97510..
term root
fdff7..