proposition: Lemma binds_dom_contradiction: forall (E : list (asn A B)), binds x a E -> x `notin` dom E -> False.
proof: Proof. clear. induction E as [ | a1 E' ]; simpl. intros H. inversion H. unfold binds in *. simpl. intros [H | H] J. inversion H; subst. fsetdec. apply IHE' in H. trivial. destruct a1. fsetdec. auto. Qed.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.MetatheoryAtom Metalib.LibTactics