proposition: Lemma Canon_Succ beta n: Canon (E0_succ beta) (S n) = beta.
proof: Proof. destruct beta. simpl. unfold E0_succ. simpl. apply E0_eq_intro. simpl. now rewrite (canon_succ). Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)