proposition: Lemma pred_of_limit : forall alpha, nf alpha -> T1limit alpha -> pred alpha = None.
proof: Proof. intros; induction alpha. - reflexivity. - simpl; destruct alpha1. + destruct n; simpl in H0; discriminate. + destruct (T1limit_cases H H0). * destruct a. subst. reflexivity. * destruct a; rewrite IHalpha2;auto. eauto with T1. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)