proposition: Lemma list_filter_subseteq P `{!∀ x : A, Decision (P x)} l : filter P l ⊆ l.
proof: Proof. induction l as [|x l IHl]; [done|]. rewrite filter_cons. destruct (decide (P x)); [by apply list_subseteq_skip|by apply list_subseteq_cons]. Qed.
imports: stdpp(options)