proposition: Lemma slifting_alifting_stateFMT (S : UU0) (t := [the fmt of stateT S]) : slifting aop t naturality_MK = alifting aop (Lift t M).
proof: Proof. apply nattrans_ext => X. rewrite (slifting_stateT aop naturality_MK S). apply funext => m; apply funext => s. rewrite /alifting. rewrite /=. rewrite psiE /=. rewrite /bindS. rewrite vcompE/=. rewrite /liftS/=. rewrite 2!algebraic. congr (aop _ _). rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. congr ((E # _) m). apply funext => x /=. by rewrite 2!bindretf. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer