proposition: Theorem map_iterate : forall (A:Set)(f:A->A)(x:A), EqSt (iterate f (f x)) (map f (iterate f x)).
proof: Proof. intros A f x. apply park_ppl with (R:= fun s1 s2 => exists x: A, s1 = iterate f (f x) /\ s2 = map f (iterate f x)). intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity. intros s1 s2 (x0,(eqs1,eqs2)). exists (f x0);split;[rewrite eqs1|rewrite eqs2]; reflexivity. exists x;split; reflexivity. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool