proposition: Lemma list_filter_filter (P1 P2 : A → Prop) `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) : filter P1 (filter P2 l) = filter (λ a, P1 a ∧ P2 a) l.
proof: Proof. induction l as [|x l IH]; [done|]. rewrite !filter_cons. case (decide (P2 x)) as [HP2|HP2]. - rewrite filter_cons, IH. apply decide_ext. naive_solver. - rewrite IH. symmetry. apply decide_False. by intros [_ ?]. Qed.
imports: stdpp(options)