proposition: Lemma iter_proper: forall f1 f2, (forall x, f1 x = f2 x) -> forall b, iter f1 b = iter f2 b.
proof: Proof. induction b. - reflexivity. - simpl. rewrite IHb. apply H. Qed.
imports: Arith Lia List FunctionalExtensionality