proposition: Lemma insert_cat (A : UU0) h (a b : seq A) u : insert h (a ++ u :: b) = (do x <- insert h a; Ret (x ++ u :: b))%Do [~] (do x <- insert h b; Ret (a ++ u :: x))%Do :> M _.
proof: Proof. elim: a h u b => [h u b|a1 a2 ih h u b]. by rewrite /= (insertE h nil) bindretf insertE fmapE. rewrite cat_cons [in LHS]insertE [u :: b]lock /= -lock [in LHS]ih. rewrite [in RHS]insertE [in RHS]alt_bindDl bindretf -altA; congr (_ [~] _). rewrite [in RHS]bind_fmap [in LHS]fmapE [in LHS]alt_bindDl !bindA. by congr (_ [~] _); under eq_bind do rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)