Apply ax_frege58b__ax_frege58b_b__df_bcc__df_addr__df_subr__df_mulv__df_ptdf__df_rr3__df_line3__df_vd1__df_vd2__df_vhc2__df_vhc3__df_vd3__df_liminf__df_xlim__df_salg__df_salon with ∀ x0 x1 x2 : ο . wb (wvd2 x0 x1 x2) (wa x0 x1 ⟶ x2).

Assume H0: ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ wsb (λ x2 . x0 x2) x1.

Assume H1: ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ wsb (λ x2 . x0 x2) x1.

Assume H2: wceq cbcc (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn0) (λ x0 x1 . co (co (cv x0) (cv x1) cfallfac) (cfv (cv x1) cfa) cdiv)).

Assume H3: wceq cplusr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cr) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) caddc))).

Assume H4: wceq cminusr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cr) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cmin))).

Assume H5: wceq ctimesr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cr) (λ x2 . co (cv x0) (cfv (cv x2) (cv x1)) cmul))).

Assume H6: ∀ x0 x1 : ι → ο . wceq (cptdfc x0 x1) (cmpt (λ x2 . cr) (λ x2 . cima (co (co (cv x2) (co x1 x0 cminusr) ctimesr) x0 cpv) (ctp c1 c2 c3))).

Assume H7: wceq crr3c (co cr (ctp c1 c2 c3) cmap).

Assume H8: wceq cline3 (crab (λ x0 . wa (wbr c2o (cv x0) cdom) (wral (λ x1 . wral (λ x2 . wne (cv x2) (cv x1) ⟶ wceq (crn (cptdfc (cv x1) (cv x2))) (cv x0)) (λ x2 . cv x0)) (λ x1 . cv x0))) (λ x0 . cpw crr3c)).

Assume H9: ∀ x0 x1 : ο . wb (wvd1 x0 x1) (x0 ⟶ x1).

Assume H10: ∀ x0 x1 x2 : ο . wb (wvd2 x0 x1 x2) (wa x0 x1 ⟶ x2).

Assume H11: ∀ x0 x1 : ο . wb (wvhc2 x0 x1) (wa x0 x1).

Assume H12: ∀ x0 x1 x2 : ο . wb (wvhc3 x0 x1 x2) (w3a x0 x1 x2).

Assume H13: ∀ x0 x1 x2 x3 : ο . wb (wvd3 x0 x1 x2 x3) (w3a x0 x1 x2 ⟶ x3).

Assume H14: wceq clsi (cmpt (λ x0 . cvv) (λ x0 . ...)).

...

■

Proofgold Proof