proposition: Lemma lt_omega_inv: forall alpha:E0, alpha o< E0_omega -> exists (i:nat), alpha = E0fin i.
proof: Proof. destruct alpha; unfold E0_omega; cbn in *; intro. destruct H. destruct H0. cbn in H0. assert (H2 : cnf0 t1< T1omega). { split; cbn in H1; tauto. } destruct (lt_omega_inv H2). - exists 0; subst; unfold E0fin; apply E0_eq_intro; reflexivity. - destruct H3; subst; exists (S x); apply E0_eq_intro; reflexivity. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)