Apply df_rnghom__df_rngiso__df_ric__df_drng__df_field__df_subrg__df_rgspn__df_abv__df_staf__df_srng__df_lmod__df_scaf__df_lss__df_lsp__df_lmhm__df_lmim__df_lmic__df_lbs with wceq clmim (cmpt2 (λ x0 x1 . clmod) (λ x0 x1 . clmod) (λ x0 x1 . crab (λ x2 . wf1o (cfv (cv x0) cbs) (cfv (cv x1) cbs) (cv x2)) (λ x2 . co (cv x0) (cv x1) clmhm))).

Assume H0: wceq crh (cmpt2 (λ x0 x1 . crg) (λ x0 x1 . crg) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . csb (cfv (cv x1) cbs) (λ x3 . crab (λ x4 . wa (wceq (cfv (cfv (cv x0) cur) (cv x4)) (cfv (cv x1) cur)) (wral (λ x5 . wral (λ x6 . wa (wceq (cfv (co (cv x5) (cv x6) (cfv (cv x0) cplusg)) (cv x4)) (co (cfv (cv x5) (cv x4)) (cfv (cv x6) (cv x4)) (cfv (cv x1) cplusg))) (wceq (cfv (co (cv x5) (cv x6) (cfv (cv x0) cmulr)) (cv x4)) (co (cfv (cv x5) (cv x4)) (cfv (cv x6) (cv x4)) (cfv (cv x1) cmulr)))) (λ x6 . cv x2)) (λ x5 . cv x2))) (λ x4 . co (cv x3) (cv x2) cmap))))).

Assume H1: wceq crs (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wcel (ccnv (cv x2)) (co (cv x1) (cv x0) crh)) (λ x2 . co (cv x0) (cv x1) crh))).

Assume H2: wceq cric (cima (ccnv crs) (cdif cvv c1o)).

Assume H3: wceq cdr (crab (λ x0 . wceq (cfv (cv x0) cui) (cdif (cfv (cv x0) cbs) (csn (cfv (cv x0) c0g)))) (λ x0 . crg)).

Assume H4: wceq cfield (cin cdr ccrg).

Assume H5: wceq csubrg (cmpt (λ x0 . crg) (λ x0 . crab (λ x1 . wa (wcel (co (cv x0) (cv x1) cress) crg) (wcel (cfv (cv x0) cur) (cv x1))) (λ x1 . cpw (cfv (cv x0) cbs)))).

Assume H6: wceq crgspn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . cint (crab (λ x2 . wss (cv x1) ...) ...)))).

...

■

Proofgold Proof