proposition: Theorem iter_comp: forall (A B : Set) zero (f1 f2 : A -> B) g l, (forall a, g a zero = a) -> (forall a b c, g a (g b c) = g (g a b) c) -> (forall a b, g a b = g b a) -> g (iter zero f1 g l) (iter zero f2 g l) = iter zero (fun x => g (f1 x) (f2 x)) g l.
proof: Proof. intros A B zero f1 f2 g l g_zero g_trans g_sym; elim l; simpl; auto. intros a l0 H; rewrite <- H; (repeat rewrite <- g_trans). apply f_equal2 with ( f := g ); auto. (repeat rewrite g_trans); apply f_equal2 with ( f := g ); auto. Qed.
imports: List Permutation Arith