proposition: Lemma binds_unique : binds x a E -> binds x b E -> uniq E -> a = b.
proof: Proof. clear. alist induction E as [ | ? ? F IH ]. inversion 1. unfold binds. simpl. intros [J1 | J1] [J2 | J2] J3. Case "left / left". congruence. Case "left / right". assert (In x (dom F)). eapply binds_In. apply J2. injection J1; intros; subst. solve_uniq. Case "right / left". assert (In x (dom F)). eapply binds_In. apply J1. injection J2; intros; subst. solve_uniq. Case "right / right". unfold binds in *. eapply IH; trivial. solve_uniq. 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