proposition: Lemma eq_Env_dec : forall (E1 E2 : Env), {E1=E2} + {E1<>E2}.
proof: Proof. decide equality; generalize a o; decide equality; apply eq_SimpleType_dec. Defined.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)