proposition: Corollary E0_eq_iff (alpha beta: E0) : alpha = beta <-> cnf alpha = cnf beta.
proof: Proof. split. - intro; now f_equal. - intro; now apply E0_eq_intro. 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)