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