proposition: Lemma lt_omega_inv alpha : nf alpha -> alpha t2< omega -> {n:nat | alpha = fin n}.
proof: Proof. destruct alpha. - exists 0; reflexivity. - intros H H0; case (lt_cons_omega_inv H0);auto with T2. destruct 2;intros; exists (S n);auto with T2. cbn; subst ; auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)