Proofgold Proposition

wceq cslmd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wa (wcel (cv x4) csrg) (wral (λ x8 . wral (λ x9 . wral (λ x10 . wral (λ x11 . wa (w3a (wcel (co (cv x9) (cv x11) (cv x3)) (cv x1)) (wceq (co (cv x9) (co (cv x11) (cv x10) (cv x2)) (cv x3)) (co (co (cv x9) (cv x11) (cv x3)) (co (cv x9) (cv x10) (cv x3)) (cv x2))) (wceq (co (co (cv x8) (cv x9) (cv x6)) (cv x11) (cv x3)) (co (co (cv x8) (cv x11) (cv x3)) (co (cv x9) (cv x11) (cv x3)) (cv x2)))) (w3a (wceq (co (co (cv x8) (cv x9) (cv x7)) (cv x11) (cv x3)) (co (cv x8) (co (cv x9) (cv x11) (cv x3)) (cv x3))) (wceq (co (cfv (cv x4) cur) (cv x11) (cv x3)) (cv x11)) (wceq (co (cfv (cv x4) c0g) (cv x11) (cv x3)) (cfv (cv x0) c0g)))) (λ x11 . cv x1)) (λ x10 . cv x1)) (λ x9 . cv x5)) (λ x8 . cv x5))) (cfv (cv x4) cmulr)) (cfv (cv x4) cplusg)) (cfv (cv x4) cbs)) (cfv (cv x0) csca)) (cfv (cv x0) cvsca)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . ccmn))

type
prop

theory
SetMM

name
df_slmd

proof
PUeuA..

Megalodon
-

proofgold address
TMTUM..

creator
36386 PrCmT../cf07d..

owner
36386 PrCmT../cf07d..

term root
4807e..