proposition: Lemma H'_eq3 alpha i : E0limit alpha -> H'_ alpha i = H'_ (Canon alpha (S i)) i.
proof: Proof. intros;rewrite H'__equation_1. destruct (E0_eq_dec alpha E0zero). - subst; discriminate. - cbn; destruct (Utils.dec (E0limit alpha)) . + now cbn. + red in H; rewrite e in H; discriminate. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)