Apply df_lvec__df_sra__df_rgmod__df_lidl__df_rsp__df_2idl__df_lpidl__df_lpir__df_nzr__df_rlreg__df_domn__df_idom__df_pid__df_assa__df_asp__df_ascl__df_psr__df_mvr with wceq c2idl (cmpt (λ x0 . cvv) (λ x0 . cin (cfv (cv x0) clidl) (cfv (cfv (cv x0) coppr) clidl))).

Assume H0: wceq clvec (crab (λ x0 . wcel (cfv (cv x0) csca) cdr) (λ x0 . clmod)).

Assume H1: wceq csra (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . co (co (co (cv x0) (cop (cfv cnx csca) (co (cv x0) (cv x1) cress)) csts) (cop (cfv cnx cvsca) (cfv (cv x0) cmulr)) csts) (cop (cfv cnx cip) (cfv (cv x0) cmulr)) csts))).

Assume H2: wceq crglmod (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cbs) (cfv (cv x0) csra))).

Assume H3: wceq clidl (ccom clss crglmod).

Assume H4: wceq crsp (ccom clspn crglmod).

Assume H5: wceq c2idl (cmpt (λ x0 . cvv) (λ x0 . cin (cfv (cv x0) clidl) (cfv (cfv (cv x0) coppr) clidl))).

Assume H6: wceq clpidl (cmpt (λ x0 . crg) (λ x0 . ciun (λ x1 . cfv (cv x0) cbs) (λ x1 . csn (cfv (csn (cv x1)) (cfv (cv x0) crsp))))).

Assume H7: wceq clpir (crab (λ x0 . wceq (cfv (cv x0) clidl) (cfv (cv x0) clpidl)) (λ x0 . crg)).

Assume H8: wceq cnzr (crab (λ x0 . wne (cfv (cv x0) cur) (cfv (cv x0) c0g)) (λ x0 . crg)).

Assume H9: wceq crlreg (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cfv (cv x0) cmulr)) (cfv (cv x0) c0g) ⟶ wceq (cv x2) (cfv (cv x0) c0g)) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs))).

Assume H10: wceq cdomn (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cfv (cv x0) cmulr)) (cv x2) ⟶ wo (wceq (cv x3) (cv x2)) (wceq (cv x4) (cv x2))) ...) ...) ...) ...) ...).

...

■

Proofgold Proof