proposition: Lemma iterate_ext2 {A:Type} (f g : (A -> A) -> A -> A) (h i : A->A) : (forall x, h x = i x) -> (forall h' i', (forall x, h' x = i' x) -> forall x, f h' x = g i' x) -> forall n x, iterate f n h x = iterate g n i x.
proof: Proof. induction n. - intros; simpl; auto. - intros; simpl; apply H0. auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)