proposition: Lemma binds_lookup : {a : A | binds x a E} + (forall a, ~ binds x a E).
proof: Proof. Proof with intuition eauto. clear. intros. alist induction E as [ | x1 a1 ? [[a' J] | J] ]... destruct (X.eq_dec x x1)... right. unfold binds. intros a' [K | ?]... unfold X.eq in *. injection K... 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