proposition: Lemma insert_map (A B : UU0) (f : A -> B) (a : A) : insert (f a) \o map f = map f (o) insert a :> (_ -> M _).
proof: Proof. apply boolp.funext; elim => [|y xs IH]. by rewrite fcompE insertE -(compE (fmap (map f))) (natural ret) compE insertE. apply/esym. rewrite fcompE insertE alt_fmapDr. rewrite -(compE (fmap (map f))) (natural ret) FIdE [in X in X [~] _ ]/=. rewrite -fmap_oE (_ : map f \o cons y = cons (f y) \o map f) //. by rewrite fmap_oE -(fcompE (map f)) -IH [RHS]/= insertE. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)