proposition: Theorem map_iterate' : forall (A:Set)(f:A->A)(x:A), EqSt (iterate f (f x)) (map f (iterate f x)).
proof: Proof. infiniteproof map_iterate'. reflexivity. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool