proposition: Lemma find_def : forall (p:A->bool) (l:list A) (x:A), find p l = Some x -> p x = true.
proof: Proof. intros p l x H. induction l. discriminate H. simpl in H. assert (p a = true \/ p a = false). case (p a); auto. elim H0; intro Hpa; rewrite Hpa in H. congruence. auto. Qed.
imports: Coq(List Arith)