proposition: Lemma eq_find_first_exact : forall l x z, find_first (eq x) (eq_dec x) l = Some z -> l[z] = Some x.
proof: Proof. intro; intro. induction l; intros; simpl in *. discr. destruct (eq_dec x a); subst. inversion H; subst; auto with *. assert (exists i, find_first (eq x) (eq_dec x) l = Some i). destruct (find_first (eq x) (eq_dec x) l); try discr. exists n0; auto with *. destruct H0. ded (IHl _ H0). rewrite H0 in H. destruct z; inversion H; subst; hyp. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)