proposition: Lemma CanonS_lt : forall i alpha, alpha <> E0zero -> Canon alpha (S i) o< alpha.
proof: Proof. destruct alpha. unfold E0lt. cbn. intro;apply canonS_LT; auto. intro H0; subst. apply H. unfold E0zero; f_equal. apply nf_proof_unicity. Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)