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 (walsc (λ x2 . x0 x2) (λ x2 . x1 x2)) (wa (wral (λ x2 . x0 x2) (λ x2 . x1 x2)) (wex (λ x2 . wcel (cv x2) (x1 x2)))).