proposition: Lemma cnf_Omega_term (alpha: E0) (n: nat) : cnf (Omega_term alpha n) = omega_term (cnf alpha) n.
proof: Proof. reflexivity. 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)