proposition: Lemma Succ_inj alpha beta : E0_succ alpha = E0_succ beta -> alpha = beta.
proof: Proof. destruct alpha, beta; intros; apply E0_eq_intro. cbn; unfold E0_succ in H; cbn in H; injection H. intro; apply succ_injective; auto. 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)