proposition: Theorem skipn_In : forall (A : Type) n ls (a : A), In a (skipn n ls) -> In a ls.
proof: Proof. induction n; destruct ls; intuition idtac. simpl in *. right. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation