proposition: Lemma Succ_rw : forall alpha, cnf (E0_succ alpha) = T1.succ (cnf alpha).
proof: Proof. now destruct alpha. 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)