proposition: Lemma handle_stateTE (X : UU0) : (slifting handle [the fmt of stateT S] naturality_MK) X = @handle_stateT' X.
proof: Proof. by rewrite slifting_stateT; apply funext => -[m f]. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model