proposition: Lemma Canon_of_limit_not_null : forall i alpha, E0limit alpha -> Canon alpha (S i) <> E0zero.
proof: Proof. destruct alpha;simpl; unfold Canon; simpl; rewrite E0_eq_iff. simpl; apply T1limit_canonS_not_zero; auto. Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)