Apply df_bigo__df_blen__df_dig__df_setrecs__df_pg__df_gte__df_gt__df_sinh__df_cosh__df_tanh__df_sec__df_csc__df_cot__df_logbALT__df_reflexive__df_irreflexive__df_alsi__df_alsc with ∀ x0 x1 : ι → ο . wb (walsi (λ x2 . x0 x2) (λ x2 . x1 x2)) (wa (∀ x2 . x0 x2 ⟶ x1 x2) (wex (λ x2 . x0 x2))).

Assume H0: wceq cbigo (cmpt (λ x0 . co cr cr cpm) (λ x0 . crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (cv x4) (cv x1)) (co (cv x3) (cfv (cv x4) (cv x0)) cmul) cle) (λ x4 . cin (cdm (cv x1)) (co (cv x2) cpnf cico))) (λ x3 . cr)) (λ x2 . cr)) (λ x1 . co cr cr cpm))).

Assume H1: wceq cblen (cmpt (λ x0 . cvv) (λ x0 . cif (wceq (cv x0) cc0) c1 (co (cfv (co c2 (cfv (cv x0) cabs) clogb) cfl) c1 caddc))).

Assume H2: wceq cdig (cmpt (λ x0 . cn) (λ x0 . cmpt2 (λ x1 x2 . cz) (λ x1 x2 . co cc0 cpnf cico) (λ x1 x2 . co (cfv (co (co (cv x0) (cneg (cv x1)) cexp) (cv x2) cmul) cfl) (cv x0) cmo))).

Assume H3: ∀ x0 : ι → ο . wceq (csetrecs x0) (cuni (cab (λ x1 . ∀ x2 . (∀ x3 . wss (cv x3) (cv x1) ⟶ wss (cv x3) (cv x2) ⟶ wss (cfv (cv x3) x0) (cv x2)) ⟶ wss (cv x1) (cv x2)))).

Assume H4: wceq cpg (csetrecs (cmpt (λ x0 . cvv) (λ x0 . cxp (cpw (cv x0)) (cpw (cv x0))))).

Assume H5: wceq cge_real (ccnv cle).

Assume H6: wceq cgt (ccnv clt).

Assume H7: wceq csinh (cmpt (λ x0 . cc) (λ x0 . co (cfv (co ci (cv x0) cmul) csin) ci cdiv)).

Assume H8: wceq ccosh (cmpt (λ x0 . cc) (λ x0 . cfv (co ci (cv x0) cmul) ccos)).

Assume H9: wceq ctanh (cmpt (λ x0 . cima (ccnv ccosh) (cdif cc (csn cc0))) (λ x0 . co (cfv (co ci (cv x0) cmul) ctan) ci cdiv)).

Assume H10: wceq csec (cmpt (λ x0 . crab (λ x1 . wne (cfv (cv x1) ccos) cc0) (λ x1 . cc)) ...).

...

■

Proofgold Proof