proposition: Lemma insert_rcons a' s : insert a (rcons s a') = Ret (s ++ [:: a'; a]) [~] fmap (rcons^~ a') (insert a s) :> M _.
proof: Proof. elim: s a' => [a'|s1 s2 IH a']. rewrite cat0s fmapE bindretf insertE altC; congr (_ [~] _). by rewrite insertE fmapE bindretf. rewrite [in LHS]/= insertE IH. rewrite alt_fmapDr [in X in _ [~] X = _]fmapE bindretf. rewrite alt_fmapDr [in X in _ = _ [~] X]fmapE bindretf. by rewrite -!fmap_oE altCA. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)