proposition: Lemma iperm_filter : iperm \o filter p = filter p (o) iperm :> (_ -> M _).
proof: Proof. apply boolp.funext; elim => [|h t /= IH]. by rewrite fcompE fmapE bindretf. case: ifPn => ph. rewrite [in LHS]/= IH [in LHS]fcomp_def compE [in LHS]bind_fmap. rewrite [in RHS]fcomp_def compE -/(fmap _ _) [in RHS]fmap_bind; bind_ext => s. by rewrite filter_insertT. rewrite fcompE fmap_bind IH fcompE fmapE; bind_ext => s. by rewrite filter_insertN. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)