proposition: Lemma E0_eq_intro : forall alpha beta : E0, cnf alpha = cnf beta -> alpha = beta.
proof: Proof. destruct alpha, beta; simpl; intros; subst; f_equal; auto; apply nf_proof_unicity. 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)