proposition: Theorem nth_firstIndexOf : forall (A : Set)(eqd : eq_dec A)(ls : list A)(a : A)(def : nat), In a ls -> nth_option ls (firstIndexOf eqd ls a def) = Some a.
proof: Proof. induction ls; intuition; simpl in *. intuition. intuition. subst. destruct (eqd a0 a0); subst; intuition. destruct (eqd a0 a); subst; intuition. Qed.
imports: FCF.FCF