proposition: Theorem iter_ext: forall (A B : Set) zero (f1 : A -> B) f2 g l, (forall a, In a l -> f1 a = f2 a) -> iter zero f1 g l = iter zero f2 g l.
proof: Proof. intros A B zero f1 f2 g l; elim l; simpl; auto. intros a l0 H H0; apply f_equal2 with ( f := g ); auto. Qed.
imports: List Permutation Arith