proposition: Lemma slifting_alifting_envFMT (Env : UU0) (t := [the fmt of envT Env]) : slifting aop t naturality_MK = alifting aop (Lift t M).
proof: Proof. apply nattrans_ext => X. rewrite (slifting_envT aop naturality_MK Env). apply funext => m; apply funext => e. rewrite /alifting. rewrite /=. rewrite psiE /= /bindEnv. rewrite vcompE/=. rewrite /liftEnv. rewrite algebraic. congr (aop _ _). rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. congr ((E # _) m). apply funext => x /=. by rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer