proposition: Lemma eq_EPS_dec : forall (a b : Env * Preterm * SimpleType), {a=b} + {a<>b}.
proof: Proof. decide equality. apply eq_SimpleType_dec. generalize a p; decide equality. apply eq_Preterm_dec. apply eq_Env_dec. Defined.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)