proposition: Lemma binds_cons_uniq_1 : uniq ((y, b) :: E) -> binds x a ((y, b) :: E) -> (x = y /\ a = b /\ ~ In x (dom E)) \/ (binds x a E /\ x <> y).
proof: Proof. clear. intros J1 J2. change ((y, b) :: E) with (y ~ b ++ E) in J1. change ((y, b) :: E) with (y ~ b ++ E) in J2. eapply binds_app_uniq_1 in J1; [ | eassumption ]. destruct J1 as [[J3 ?] | [? ?]]. unfold binds in J3. simpl in J3. destruct J3 as [J4 | ]. injection J4. intros. subst. auto. intuition. simpl in *. right. split; [ trivial | fsetdec ]. 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