Proofgold Proposition

wceq ccusp (crab (λ x0 . wral (λ x1 . wcel (cv x1) (cfv (cfv (cv x0) cuss) ccfilu) ⟶ wne (co (cfv (cv x0) ctopn) (cv x1) cflim) c0) (λ x1 . cfv (cfv (cv x0) cbs) cfil)) (λ x0 . cusp))

type
prop

theory
SetMM

name
df_cusp

proof
PUNQ5..

Megalodon
-

proofgold address
TMLSt..

creator
36378 PrCmT../861b0..

owner
36378 PrCmT../861b0..

term root
a599e..