proposition: Lemma list_find_None l : list_find P l = None ↔ Forall (λ x, ¬P x) l.
proof: Proof. rewrite eq_None_not_Some, Forall_forall. split. - intros Hl x Hx HP. destruct Hl. eauto using list_find_elem_of. - intros HP [[i x] (?%elem_of_list_lookup_2&?&?)%list_find_Some]; naive_solver. Qed.
imports: stdpp(options)