proposition: Lemma eq_dec (alpha beta: t) : {alpha = beta} + {alpha <> beta}.
proof: Proof. repeat decide equality. Defined.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)