proposition: Lemma flush_outputTE (X : UU0) : (slifting flush [the fmt of outputT R] naturality_MK) X = @flush_outputT' X.
proof: Proof. by rewrite slifting_outputT; exact: funext. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model