proposition: Lemma Succ_Succb (alpha : E0) : E0is_succ (E0_succ alpha).
proof: Proof. destruct alpha; unfold E0is_succ, E0_succ; cbn; apply T1.succ_is_succ. 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)