proposition: Lemma Succb_Succ alpha : E0is_succ alpha -> {beta : E0 | alpha = E0_succ beta}.
proof: Proof. destruct alpha; cbn. intro H; destruct (T1is_succ_def cnf_ok0 H) as [beta [Hbeta Hbeta']]; subst. assert (nf (succ beta)) by eauto with T1. exists (@mkord beta Hbeta); apply E0_eq_intro; now cbn. Defined.
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)