Proofgold Proposition

wceq cnmf (cmpt (λ x0 . co cc 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)) cabs))) (λ x2 . chil))) cxr clt))

type
prop

theory
SetMM

name
df_nmfn

proof
PUUBK..

Megalodon
-

proofgold address
TMUeL..

creator
36383 PrCmT../5ca5d..

owner
36383 PrCmT../5ca5d..

term root
70f20..