proposition: Lemma find_first_Some : forall l, find_first l <> None -> exists z, In z l /\ P z.
proof: Proof. intros. induction l. simpl in H; tauto. simpl in H. destruct (P_dec a). exists a; split; simpl; tauto. destruct (find_first l); try discr. assert (exists z : A, In z l /\ P z). apply IHl; discr. destruct H0. exists x. simpl; tauto. tauto. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)