proposition: Theorem nth_option_In : forall (A : Set)(ls : list A)(a : A) i, nth_option ls i = Some a -> In a ls.
proof: Proof. induction ls; intuition; simpl in *. discriminate. destruct i. inversion H; clear H; subst. intuition. right. eapply IHls. eauto. Qed.
imports: FCF.FCF