Apply 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 with ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 cc) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cmul) x2 csm) (co x0 (co x1 x2 csm) csm).

Assume H0: wf (cxp chil chil) chil cva.

Assume H1: ∀ x0 x1 : ι → ο . wa (wcel x0 chil) (wcel x1 chil) ⟶ wceq (co x0 x1 cva) (co x1 x0 cva).

Assume H2: ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 chil) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cva) x2 cva) (co x0 (co x1 x2 cva) cva).

Assume H3: wcel c0v chil.

Assume H4: ∀ x0 : ι → ο . wcel x0 chil ⟶ wceq (co x0 c0v cva) x0.

Assume H5: wf (cxp cc chil) chil csm.

Assume H6: ∀ x0 : ι → ο . wcel x0 chil ⟶ wceq (co c1 x0 csm) x0.

Assume H7: ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 cc) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cmul) x2 csm) (co x0 (co x1 x2 csm) csm).

Assume H8: ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co x0 (co x1 x2 cva) csm) (co (co x0 x1 csm) (co x0 x2 csm) cva).

Assume H9: ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 cc) (wcel x2 chil) ⟶ wceq (co (co x0 x1 caddc) x2 csm) (co (co x0 x2 csm) (co x1 x2 csm) cva).

Assume H10: ∀ x0 : ι → ο . wcel x0 chil ⟶ wceq (co cc0 x0 csm) c0v.

Assume H11: wf (cxp chil chil) cc csp.

Assume H12: ∀ x0 x1 : ι → ο . wa (wcel x0 chil) (wcel x1 chil) ⟶ wceq (co x0 x1 csp) (cfv (co x1 x0 csp) ccj).

Assume H13: ∀ x0 x1 x2 : ι → ο . w3a (wcel ... ...) ... ... ⟶ wceq (co (co x0 x1 cva) x2 csp) (co (co x0 x2 csp) (co x1 x2 csp) caddc).

...

■

Proofgold Proof