proposition: Lemma natural_hmapE (t : fmt) (M N : monad) (n : M ~> N) (X : UU0) : hmap t n X \o Lift t M X = Lift t N X \o n X.
proof: Proof. have /nattrans_ext/(_ X)/= := @natural_hmap t M N n. by rewrite !vcompE. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib