proposition: Theorem nth_firstIndexOf_if : forall (A : Set)(eqd : eq_dec A)(ls : list A) n a, nth_option ls n = Some a -> NoDup ls -> firstIndexOf eqd ls a 0 = n.
proof: Proof. induction ls; intuition; simpl in *. discriminate. inversion H0; clear H0; subst. destruct n. inversion H; clear H; subst. destruct (eqd a0 a0); subst; intuition. destruct (eqd a0 a); subst; intuition. exfalso. eapply H3. eapply nth_option_In. eauto. Qed.
imports: FCF.FCF