Proofgold Proposition

wceq coppcc (cmpt (λ x0 . cun cccbar ccchat) (λ x0 . cif (wceq (cv x0) cinfty) cinfty (cif (wcel (cv x0) cc) (cneg (cv x0)) (cfv (cif (wbr cc0 (cfv (cv x0) c1st) clt) (co (cfv (cv x0) c1st) cpi cmin) (co (cfv (cv x0) c1st) cpi caddc)) cinftyexpi))))

type
prop

theory
SetMM

name
df_bj_oppc

proof
PUUUJ..

Megalodon
-

proofgold address
TMFMQ..

creator
36376 PrCmT../61f99..

owner
36376 PrCmT../61f99..

term root
3ac9e..