proposition: Lemma CanonS_phi0_lim alpha k : E0limit alpha -> Canon (E0_phi0 alpha) (S k) = E0_phi0 (Canon alpha (S k)).
proof: Proof. intro; orefl; rewrite cnf_phi0. unfold Canon; repeat rewrite cnf_rw; rewrite <- canonS_lim1. - now rewrite cnf_phi0. - apply cnf_ok. - destruct alpha; cbn; assumption. Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)