Apply df_md__df_dmd__df_at__df_dp2__df_dp__df_xdiv__ax_xrssca__ax_xrsvsca__df_omnd__df_ogrp__df_sgns__df_inftm__df_archi__df_slmd__df_orng__df_ofld__df_resv__df_smat with wceq cdp (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cr) (λ x0 x1 . cdp2 (cv x0) (cv x1))).

Assume H0: wceq cmd (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wral (λ x2 . wss (cv x2) (cv x1) ⟶ wceq (cin (co (cv x2) (cv x0) chj) (cv x1)) (co (cv x2) (cin (cv x0) (cv x1)) chj)) (λ x2 . cch)))).

Assume H1: wceq cdmd (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wral (λ x2 . wss (cv x1) (cv x2) ⟶ wceq (co (cin (cv x2) (cv x0)) (cv x1) chj) (cin (cv x2) (co (cv x0) (cv x1) chj))) (λ x2 . cch)))).

Assume H2: wceq cat (crab (λ x0 . wbr c0h (cv x0) ccv) (λ x0 . cch)).

Assume H3: ∀ x0 x1 : ι → ο . wceq (cdp2 x0 x1) (co x0 (co x1 (cdc c1 cc0) cdiv) caddc).

Assume H4: wceq cdp (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cr) (λ x0 x1 . cdp2 (cv x0) (cv x1))).

Assume H5: wceq cxdiv (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cdif cr (csn cc0)) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) cxmu) (cv x0)) (λ x2 . cxr))).

Assume H6: wceq crefld (cfv cxrs csca).

Assume H7: wceq cxmu (cfv cxrs cvsca).

Assume H8: wceq comnd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wcel (cv x0) ctos) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wbr (cv x4) (cv x5) (cv x3) ⟶ wbr (co (cv x4) (cv x6) (cv x2)) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1))) (cfv (cv x0) cple)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . cmnd)).

Assume H9: wceq cogrp (cin cgrp comnd).

Assume H10: wceq csgns (cmpt ... ...).

...

■

Proofgold Proof