proposition: Lemma filter_app_complement l : filter P l ++ filter (λ x, ¬P x) l ≡ₚ l.
proof: Proof. induction l as [|x l IH]; simpl; [done|]. case_decide. - rewrite decide_False by naive_solver. simpl. by rewrite IH. - rewrite decide_True by done. by rewrite <-Permutation_middle, IH. Qed.
imports: stdpp(options)