proposition: Theorem nth_In_exists : forall (A : Type)(ls : list A) a def, In a ls -> exists n, nth n ls def = a.
proof: Proof. induction ls; intuition; simpl in *. intuition. intuition; subst. exists O. trivial. edestruct IHls. eauto. exists (S x). eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation