proposition: Lemma binds_app_uniq : uniq (E ++ F) -> (binds x a (E ++ F) <-> (binds x a E /\ x `notin` dom F) \/ (binds x a F /\ x `notin` dom E)).
proof: Proof. Proof with intuition (fsetdec || eauto using binds_dom_contradiction). clear. intros H1. autorewrite with rewr_uniq in H1. unfold disjoint in H1. assert (H : x `notin` dom F \/ x `notin` dom E) by fsetdec. rewrite binds_app... Qed.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.MetatheoryAtom Metalib.LibTactics