Search for blocks/addresses/...

Proofgold Proposition

wceq cmarrep (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt2 (λ x2 x3 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cmpt2 (λ x4 x5 . cv x0) (λ x4 x5 . cv x0) (λ x4 x5 . cmpt2 (λ x6 x7 . cv x0) (λ x6 x7 . cv x0) (λ x6 x7 . cif (wceq (cv x6) (cv x4)) (cif (wceq (cv x7) (cv x5)) (cv x3) (cfv (cv x1) c0g)) (co (cv x6) (cv x7) (cv x2)))))))
type
prop
theory
SetMM
name
df_marrep
proof
PUTDz..
Megalodon
-
proofgold address
TMVeL..
creator
36386 PrCmT../459a2..
owner
36386 PrCmT../459a2..
term root
edcb1..