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