proposition: Theorem iter_comp_const: forall (A B : Set) zero (f : A -> B) g k l, k zero = zero -> (forall a b, k (g a b) = g (k a) (k b)) -> k (iter zero f g l) = iter zero (fun x => k (f x)) g l.
proof: Proof. intros A B zero f g k l H H0; elim l; simpl; auto. intros a l0 H1; rewrite H0; apply f_equal2 with ( f := g ); auto. Qed.
imports: List Permutation Arith