proposition: Lemma LT_succ_LT_eq_dec : forall alpha beta, nf alpha -> nf beta -> alpha t1< succ beta -> {alpha t1< beta} + {alpha = beta}.
proof: Proof. intros. destruct H1 as [H2 [H3 H4]]. generalize (lt_succ_le_2 H H0 H3). intro. apply le_eq_lt_dec in H1 as [Heq | Hlt]. - now right. - left; repeat split; auto. Defined.
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)