proposition: Lemma binds_lookup_dec : decidable (exists a, binds x a E).
proof: Proof. Proof with intuition eauto. clear. intros. unfold decidable. destruct binds_lookup as [[? ?] | ?]... right. intros [? ?]... 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