proposition: Lemma Forall_list_intersection `{!EqDecision A} l k : Forall P l → Forall P (list_intersection l k).
proof: Proof. rewrite !Forall_forall. intros ? x; rewrite elem_of_list_intersection; naive_solver. Qed.
imports: stdpp(options)