proposition: Lemma map_length : forall (A B : Set) (f : A -> B) (l : list A), length A l = length B (map A B f l).
proof: Proof. simple induction l. simpl in |- *. reflexivity. simpl in |- *. intros. rewrite H. reflexivity. Qed.
imports: Arith ZArith EqNat dec natZ