proposition: Theorem skipn_map_eq : forall (A B : Type)(n : nat)(ls : list A)(f : A -> B), skipn n (map f ls) = map f (skipn n ls).
proof: Proof. induction n; destruct ls; intuition idtac; simpl in *. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation