proposition: Lemma find_first_ok : forall l p, find_first l = Some p -> exists el, nth_error l p = Some el /\ P el.
proof: Proof. induction l. inversion 1. simpl. destruct (P_dec a). intros q q0. inversion q0. exists a; split; trivial. destruct p. destruct (find_first l); inversion 1. intros pl. destruct (IHl p) as [el [lp Pl]]. destruct (find_first l); inversion pl; trivial. exists el; split; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)