proposition: Lemma filter_insertN a : ~~ p a -> forall s, (filter p (o) insert a) s = Ret (filter p s) :> M _.
proof: Proof. move=> pa; elim => [|h t IH]. by rewrite fcompE insertE -(compE (fmap _)) (natural ret) FIdE /= (negbTE pa). rewrite fcompE insertE alt_fmapDr. rewrite -(compE (fmap _)) (natural ret) FIdE [in X in X [~] _]/= (negbTE pa). case: ifPn => ph. - rewrite -fmap_oE (_ : filter p \o cons h = cons h \o filter p); last first. by apply funext => x /=; rewrite ph. rewrite fmap_oE. move: (IH); rewrite fcompE => ->. by rewrite fmapE /= ph bindretf /= Mmm. - rewrite -fmap_oE (_ : filter p \o cons h = filter p); last first. by apply funext => x /=; rewrite (negbTE ph). by move: (IH); rewrite fcompE => -> /=; rewrite (negbTE ph) Mmm. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)