proposition: Lemma iperm_insert {A : UU0} a b (s t : seq A) : (do x <- iperm (b :: s ++ t); insert a x = do x <- iperm (rcons s a ++ t); insert b x :> M _)%Do.
proof: Proof. elim: s => [/=|h tl ih] in a b t *. rewrite !bindA. by under eq_bind do rewrite insertC. rewrite [h :: tl]lock /= -lock ih /= !bindA. suff : (do x <- iperm (rcons tl b ++ t); do x0 <- insert a x; insert h x0 = do x <- iperm (rcons tl a ++ t); do x0 <- insert b x; insert h x0 :> M _)%Do. under eq_bind do rewrite insertC. move=> ->. by under eq_bind do rewrite insertC. rewrite -bindA -ih /= -bindA -[in RHS]ih /= !bindA; bind_ext => a'. by rewrite -bindA insertC bindA. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)