Proofgold Proposition

∀ x0 : ο . (wf (cxp chil chil) chil cva ⟶ (∀ x1 x2 : ι → ο . wa (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co x1 x2 cva) (co x2 x1 cva)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 chil) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co (co x1 x2 cva) x3 cva) (co x1 (co x2 x3 cva) cva)) ⟶ wcel c0v chil ⟶ (∀ x1 : ι → ο . wcel x1 chil ⟶ wceq (co x1 c0v cva) x1) ⟶ wf (cxp cc chil) chil csm ⟶ (∀ x1 : ι → ο . wcel x1 chil ⟶ wceq (co c1 x1 csm) x1) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 cc) (wcel x3 chil) ⟶ wceq (co (co x1 x2 cmul) x3 csm) (co x1 (co x2 x3 csm) csm)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co x1 (co x2 x3 cva) csm) (co (co x1 x2 csm) (co x1 x3 csm) cva)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 cc) (wcel x3 chil) ⟶ wceq (co (co x1 x2 caddc) x3 csm) (co (co x1 x3 csm) (co x2 x3 csm) cva)) ⟶ (∀ x1 : ι → ο . wcel x1 chil ⟶ wceq (co cc0 x1 csm) c0v) ⟶ wf (cxp chil chil) cc csp ⟶ (∀ x1 x2 : ι → ο . wa (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co x1 x2 csp) (cfv (co x2 x1 csp) ccj)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 chil) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co (co x1 x2 cva) x3 csp) (co (co x1 x3 csp) (co x2 x3 csp) caddc)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co (co x1 x2 csm) x3 csp) (co x1 (co x2 x3 csp) cmul)) ⟶ (∀ x1 : ι → ο . wa (wcel x1 chil) (wne x1 c0v) ⟶ wbr cc0 (co x1 x1 csp) clt) ⟶ (∀ x1 : ι → ο . wcel x1 ccau ⟶ wrex (λ x2 . wbr x1 (cv x2) chli) (λ x2 . chil)) ⟶ wceq csh (crab (λ x1 . w3a (wcel c0v (cv x1)) (wss (cima cva (cxp (cv x1) (cv x1))) (cv x1)) (wss (cima csm (cxp cc (cv x1))) (cv x1))) (λ x1 . cpw chil)) ⟶ x0) ⟶ x0

type
prop

theory
SetMM

name
ax_hfvadd__ax_hvcom__ax_hvass__ax_hv0cl__ax_hvaddid__ax_hfvmul__ax_hvmulid__ax_hvmulass__ax_hvdistr1__ax_hvdistr2__ax_hvmul0__ax_hfi__ax_his1__ax_his2__ax_his3__ax_his4__ax_hcompl__df_sh

proof
PUV1k..

Megalodon
-

proofgold address
TMdLw..

creator
36224 PrCmT../283d6..

owner
36224 PrCmT../283d6..

term root
cc5b8..