proposition: Lemma find_first_exact : forall l i, find_first l = Some i -> exists z, l[i] = Some z /\ P z.
proof: Proof. induction l; intros. simpl in H. discr. simpl in H. destruct (P_dec a). inversion H. exists a; subst; simpl; tauto. destruct (find_first l); try discr. inversion H; subst. simpl. apply IHl; auto. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)