proposition: Lemma iperm_insertC (A : eqType) x y (s : seq A) : (do s' <- iperm (rcons s x); insert y s' = do s' <- insert y s; iperm (rcons s' x) :> M _)%Do.
proof: Proof. have [n ns] := ubnP (size s); elim: n s ns x y => // n ih. move=> [/= _ x y|h t]. by rewrite !bindA !bindretf /= bindA bindretf [in RHS]insertE bindretf. rewrite ltnS /= => tn x y. rewrite bindA iperm_rcons /= !bindA [in RHS]insertE alt_bindDl bindretf /=. rewrite bindA iperm_rcons /= bindA bind_fmap /comp /= -[in X in _ [~]X]bindA. rewrite -ih// bindA iperm_rcons /= !bindA -alt_bindDr; bind_ext => s'. rewrite -alt_bindDr; bind_ext => t'. by rewrite insertC altmm. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)