proposition: Lemma binds_split : binds x a G -> exists G1 G2, G = G2 ++ one (x, a) ++ G1.
proof: Proof. clear. intro HB. induction G. + inversion HB. + destruct a0 as [y b]. apply binds_cons_1 in HB. destruct HB as [[E1 E2]|E]. subst. ++ exists l. exists nil. simpl_alist. auto. ++ destruct (IHl E) as [G1 [G2 E2]]. subst. eexists. exists ((y ~ b) ++ G2). simpl_alist. eauto. 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