proposition: Lemma slifting_alifting_exceptFMT (Z : UU0) (t := [the fmt of exceptT Z]) : slifting aop t naturality_MK = alifting aop (Lift t M).
proof: Proof. apply nattrans_ext => X. rewrite (slifting_exceptT aop naturality_MK Z). apply funext => m. rewrite /alifting. rewrite /=. rewrite psiE /= /bindX. rewrite vcompE/=. rewrite /liftX. rewrite 2!algebraic. congr (aop _ _). rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. rewrite (_ : _ \o Ret = id) ?functor_id //. apply funext => n /=. by rewrite 2!bindretf. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer