proposition: Lemma L4 : T1limit alpha.
proof: Proof. destruct (zero_limit_succ_dec Halpha) as [[Hzero | Hlim] | Hsucc]. - now destruct HnonZero. - assumption. - destruct Hsucc as [beta [Hbeta e]]; subst; destruct (H beta). + now apply LT_succ. + destruct (@LT_succ_LT_eq_dec x beta); auto. * destruct H0; eauto with T1. * destruct H0; auto. * destruct H0; assert (x t1< x) by (transitivity beta; auto). destruct (LT_irrefl H2). * subst; destruct H0. destruct (LT_irrefl H0). Qed.
imports: hydras(Epsilon0 T1) Coq(Ensembles Image Compare_dec)