proposition: Lemma filter_insertT a : p a -> filter p (o) insert a = insert a \o filter p :> (_ -> M _).
proof: Proof. move=> pa; apply funext; elim => [|h t IH]. by rewrite fcompE !insertE fmapE bindretf /= pa. rewrite fcompE [in RHS]/=; case: ifPn => ph. - rewrite [in RHS]insertE. move: (IH); rewrite [in X in X -> _]/= => <-. rewrite [in LHS]insertE alt_fmapDr; congr (_ [~] _). by rewrite fmapE bindretf /= pa ph. rewrite !fmapE /= fcompE bind_fmap bindA. under [LHS]eq_bind do rewrite bindretf. by rewrite /= ph. - rewrite [in LHS]insertE alt_fmapDr. rewrite -[in X in _ [~] X = _]fmap_oE. rewrite (_ : (filter p \o cons h) = filter p); last first. by apply funext => x /=; rewrite (negbTE ph). move: (IH); rewrite fcompE => ->. rewrite fmapE bindretf /= pa (negbTE ph) [in RHS]insertE; case: (filter _ _) => [|h' t']. by rewrite insertE Mmm. by rewrite !insertE altA Mmm. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)