Proofgold Proposition

wceq cnop (cmpt (λ x0 . co chil chil cmap) (λ x0 . csup (cab (λ x1 . wrex (λ x2 . wa (wbr (cfv (cv x2) cno) c1 cle) (wceq (cv x1) (cfv (cfv (cv x2) (cv x0)) cno))) (λ x2 . chil))) cxr clt))

type
prop

theory
SetMM

name
df_nmop

proof
PUL5f..

Megalodon
-

proofgold address
TMW21..

creator
36387 PrCmT../1af6a..

owner
36387 PrCmT../1af6a..

term root
d9e73..