proposition: Lemma E0_eq_dec : forall alpha beta: E0, {alpha = beta}+{alpha <> beta}.
proof: Proof. destruct alpha, beta. destruct (T1_eq_dec cnf0 cnf1) as [e | n]. - subst; left; auto with E0. - right; intro H; destruct n; now injection H. 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)