proposition: Theorem iter_map: forall (A B C : Set) zero (f : B -> C) g (k : A -> B) l, iter zero f g (map k l) = iter zero (fun x => f (k x)) g l.
proof: Proof. intros A B C zero f g k l; elim l; simpl; auto. intros; apply f_equal2 with ( f := g ); auto with arith. Qed.
imports: List Permutation Arith