Proofgold Proposition

wceq cxdiv (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cdif cr (csn cc0)) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) cxmu) (cv x0)) (λ x2 . cxr)))

type
prop

theory
SetMM

name
df_xdiv

proof
PUeuA..

Megalodon
-

proofgold address
TMLrd..

creator
36386 PrCmT../a80d2..

owner
36386 PrCmT../a80d2..

term root
39323..