proposition: Lemma L1 (i: nat) : beta t1< s i t1< alpha.
proof: Proof. induction i; unfold s; cbn. - split. + apply LT_add; eauto with T1; discriminate. + rewrite <- succ_is_plus_one; apply succ_lt_limit;auto. - replace (beta + FS (S i)) with (succ (beta + S i)). + destruct IHi; split. * apply LT_trans with (s i); auto. apply LT_succ; eauto with T1. * apply succ_lt_limit; auto. + rewrite succ_of_plus_finite. * reflexivity. * eauto with T1. Qed.
imports: hydras(Epsilon0 T1) Coq(Ensembles Image Compare_dec)