\r
opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
\r
opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
opt_co' env sym (CoVarCo cv)\r
| Just co <- lookupCoVar env cv\r
= opt_co (zapCvSubstEnv env) sym co\r
opt_co' env sym (CoVarCo cv)\r
| Just co <- lookupCoVar env cv\r
= opt_co (zapCvSubstEnv env) sym co\r