proposition: Lemma flush_stateTE (X : UU0) : (slifting flush [the fmt of stateT S] naturality_MK) X = @flush_stateT X.
proof: Proof. by rewrite slifting_stateT. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model