proposition: Lemma H'_Omega_term_1 : alpha <> E0zero -> forall k, H'_ (Omega_term alpha (S i)) k = H'_ (Omega_term alpha i) (H'_ (E0_phi0 alpha) k).
proof: Proof. Proof with auto with E0. intros H k; rewrite H'_eq3 ... - ochange (Canon (Omega_term alpha (S i)) (S k)) (Cons alpha i (Canon (E0_phi0 alpha) (S k))). + rewrite H'_cons ... * f_equal; rewrite (H'_eq3 (E0_phi0 alpha)) ... + rewrite cnf_Cons ... * unfold Canon. repeat rewrite cnf_rw. rewrite cnf_Omega_term, cnf_phi0. unfold Omega_term; simpl. destruct (cnf alpha) ... destruct (pred (cons t1 n t2)) ... - apply T1limit_Omega_term ... Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)