proposition: Lemma disjoint_app_1 : forall A B (E F : list (X.t*A)) (G : list (X.t*B)), disjoint (E ++ F) G -> disjoint E G.
proof: Proof. unfold disjoint. intros. rewrite dom_app in *. 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