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