proposition: Lemma list_filter_filter_r (P1 P2 : A → Prop) `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) : (∀ x, P2 x → P1 x) → filter P1 (filter P2 l) = filter P2 l.
proof: Proof. intros HPimp. rewrite list_filter_filter. apply list_filter_iff. naive_solver. Qed.
imports: stdpp(options)