proposition: Lemma binds_dec : (forall a b : A, {a = b} + {a <> b}) -> {binds x a E} + {~ binds x a E}.
proof: Proof. clear. intros. unfold binds. apply List.In_dec. decide equality. apply X.eq_dec. Defined.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Coq.Strings.String String Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.CoqFSetInterface Coq.Classes.Equivalence Coq.Classes.EquivDec Metalib.CoqEqDec