proposition: Lemma binds_In_inv : forall x (E : list (X.t*A)), In x (dom E) -> exists a, binds x a E.
proof: Proof. clear. alist induction E as [ | y b F IH ]; intros J. simpl_alist in J. fsetdec. simpl_alist in J. apply union_1 in J. destruct J as [J | J]. exists b. apply singleton_1 in J. auto. apply IH in J. destruct J. eauto. Qed.
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