proposition: Lemma alt_fmapDr (A B : UU0) (f : A -> B) (m1 m2 : M A) : (M # f) (m1 [~] m2) = (M # f) m1 [~] (M # f) m2.
proof: Proof. by rewrite 3!fmapE alt_bindDl. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)