proposition: Lemma map_firstn : forall A B l n (f : A -> B), map f (firstn n l) = firstn n (map f l).
proof: Proof. induction l; introv; simpl. - allrw firstn_nil; simpl; auto. - destruct n; simpl; auto. rw IHl; auto. Qed.
imports: UsefulTypes bin_rels Omega