proposition: Lemma find_some l x : find l = Some x -> In x l /\ f x = true.
proof: Proof. induction l as [|a l IH]; simpl; [easy| ]. case_eq (f a); intros Ha Eq. * injection Eq as [= ->]; auto. * destruct (IH Eq); auto. Qed.
imports: PeanoNat