proposition: Lemma not_in_nth_option : forall (A : Set)(ls : list A)(a : A)(i : nat), (~In a ls) -> nth_option ls i = Some a -> False.
proof: Proof. induction ls; intuition; simpl in *. discriminate. destruct i. inversion H0; clear H0; subst. intuition. eapply IHls; eauto. Qed.
imports: FCF.FCF