Apply df_fn__df_f__df_f1__df_fo__df_f1o__df_fv__df_isom__df_riota__df_ov__df_oprab__df_mpt2__df_of__df_ofr__df_rpss__ax_un__df_om__df_1st__df_2nd with
wceq com (crab (λ x0 . ∀ x1 . wlim (cv x1) ⟶ wcel (cv x0) (cv x1)) (λ x0 . con0)).
Assume H1:
∀ x0 x1 x2 : ι → ο . wb (wf x0 x1 x2) (wa (wfn x2 x0) (wss (crn x2) x1)).
Assume H2:
∀ x0 x1 x2 : ι → ο . wb (wf1 x0 x1 x2) (wa (wf x0 x1 x2) (wfun (ccnv x2))).
Assume H3:
∀ x0 x1 x2 : ι → ο . wb (wfo x0 x1 x2) (wa (wfn x2 x0) (wceq (crn x2) x1)).
Assume H4:
∀ x0 x1 x2 : ι → ο . wb (wf1o x0 x1 x2) (wa (wf1 x0 x1 x2) (wfo x0 x1 x2)).
Assume H5:
∀ x0 x1 : ι → ο . wceq (cfv x0 x1) (cio (λ x2 . wbr x0 (cv x2) x1)).
Assume H7:
∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wceq (crio (λ x2 . x0 x2) (λ x2 . x1 x2)) (cio (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))).
Assume H8:
∀ x0 x1 x2 : ι → ο . wceq (co x0 x1 x2) (cfv (cop x0 x1) x2).
Assume H10:
∀ x0 x1 x2 : ι → ι → ι → ο . wceq (cmpt2 (λ x3 x4 . x0 x3 x4) (λ x3 x4 . x1 x3 x4) (λ x3 x4 . x2 x3 x4)) (coprab (λ x3 x4 x5 . wa (wa (wcel (cv x3) (x0 x3 x4)) (wcel (cv x4) (x1 x3 x4))) (wceq (cv x5) (x2 x3 x4)))).