Apply df_fr__df_se__df_we__df_xp__df_rel__df_cnv__df_co__df_dm__df_rn__df_res__df_ima__df_pred__df_ord__df_on__df_lim__df_suc__df_iota__df_fun with
∀ x0 x1 : ι → ο . wceq (cres x0 x1) (cin x0 (cxp x1 cvv)).
Assume H2:
∀ x0 x1 : ι → ο . wb (wwe x0 x1) (wa (wfr x0 x1) (wor x0 x1)).