proposition: Lemma H'_Fin_iterate : forall i k, H'_ (E0fin (S i)) k = iterate (H'_ (E0fin 1)) (S i) k.
proof: Proof. intros; repeat rewrite H'_Fin. replace (iterate (H'_ 1) (S i) k) with (iterate S (S i) k). induction i; cbn. auto. simpl Nat.add in IHi. rewrite IHi. f_equal. apply iterate_ext. intro; rewrite H'_Fin. auto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)