Apply df_coels__df_rels__df_ssr__df_refs__df_refrels__df_refrel__df_cnvrefs__df_cnvrefrels__df_cnvrefrel__df_syms__df_symrels__df_symrel__df_prt__ax_c5__ax_c4__ax_c7__ax_c10__ax_c10_b with ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ x0 x1.

Assume H0: ∀ x0 : ι → ο . wceq (ccoels x0) (ccoss (cres (ccnv cep) x0)).

Assume H1: wceq crels (cpw (cxp cvv cvv)).

Assume H2: wceq cssr (copab (λ x0 x1 . wss (cv x0) (cv x1))).

Assume H3: wceq crefs (cab (λ x0 . wbr (cin cid (cxp (cdm (cv x0)) (crn (cv x0)))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) cssr)).

Assume H4: wceq crefrels (cin crefs crels).

Assume H5: ∀ x0 : ι → ο . wb (wrefrel x0) (wa (wss (cin cid (cxp (cdm x0) (crn x0))) (cin x0 (cxp (cdm x0) (crn x0)))) (wrel x0)).

Assume H6: wceq ccnvrefs (cab (λ x0 . wbr (cin cid (cxp (cdm (cv x0)) (crn (cv x0)))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) (ccnv cssr))).

Assume H7: wceq ccnvrefrels (cin ccnvrefs crels).

Assume H8: ∀ x0 : ι → ο . wb (wcnvrefrel x0) (wa (wss (cin x0 (cxp (cdm x0) (crn x0))) (cin cid (cxp (cdm x0) (crn x0)))) (wrel x0)).

Assume H9: wceq csyms (cab (λ x0 . wbr (ccnv (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0))))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) cssr)).

Assume H10: wceq csymrels (cin csyms crels).

Assume H11: ∀ x0 : ι → ο . wb (wsymrel x0) (wa (wss (ccnv (cin x0 (cxp (cdm x0) (crn x0)))) (cin x0 (cxp (cdm x0) (crn x0)))) (wrel x0)).

Assume H12: ∀ x0 : ι → ο . wb (wprt x0) (wral (λ x1 . wral (λ x2 . wo (wceq (cv x1) (cv x2)) (wceq (cin (cv x1) (cv x2)) c0)) (λ x2 . x0)) (λ x1 . x0)).

Assume H13: ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ x0 x1.

Assume H14: ∀ x0 x1 : ι → ο . (∀ x2 . (∀ x3 . x0 x3) ⟶ x1 x2) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . x1 x2.

Assume H15: ∀ x0 : ι → ο . ∀ x1 . wn (∀ x2 . wn (∀ x3 . ...)) ⟶ x0 x1.

...

■

Proofgold Proof