proposition: Lemma find_first_exist : forall x l, In x l -> P x -> find_first l <> None.
proof: Proof. intros. induction l. simpl in H;tauto. simpl in H. destruct H. subst; simpl. destruct (P_dec x); auto; discr. simpl. destruct (P_dec a). discr. ded (IHl H). destruct (find_first l). discr. tauto. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)