proposition: Lemma nth_lookupIndex : forall (A : Set)(eqd : eq_dec A)(ls : list A) n (a a': A), In a ls -> nth (lookupIndex eqd ls a n ) ls a' = a.
proof: Proof. induction ls; intuition; simpl in *. intuition. intuition; subst. destruct (eqd a0 a0); try congruence. destruct (eqd a0 a); subst. trivial. eauto. Qed.
imports: FCF.FCF Permutation