proposition: Lemma iterate_ext {A:Type}(f g: A -> A) (H: forall x, f x = g x): forall n x, iterate f n x = iterate g n x.
proof: Proof. induction n; simpl; auto. intro; rewrite IHn; now rewrite H. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)