proposition: Lemma eq_In_find_first : forall x l, In x l -> exists z, find_first (eq x) (eq_dec x) l = Some z /\ l[z] = Some x.
proof: Proof. intros; induction l. unfold In in H; tauto. simpl in H. destruct (eq_dec x a); subst. exists 0; split; simpl; auto with *. destruct (eq_dec a a); auto with *; tauto. destruct H; subst; try tauto. ded (IHl H); destruct H0 as [z]; destruct H0. exists (S z); split; simpl; auto with *. destruct (eq_dec x a); subst; try tauto. destruct (find_first (eq x) (eq_dec x) l); subst; try tauto; inversion H0; subst; auto. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)