proposition: Lemma binds_map_3 : binds x b0 (map f E) -> exists a, f a = b0 /\ binds x a E.
proof: Proof. alist induction E. - inversion 1. - unfold binds in *. simpl. intros [? | ?]. inversion H; subst. exists a0. auto. destruct IHl as [a1 [EQ B0]]; auto. exists a1. auto. 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