proposition: Lemma uniq_mid : forall b E' F', uniq (E ++ (x ~ a) ++ F) -> (E ++ x ~ a ++ F) = (E' ++ x ~ b ++ F') -> E = E' /\ a = b /\ F = F'.
proof: Proof. generalize F a. clear. induction E. + intros. destruct E'; inversion H0; simpl_alist in *. auto. subst. destruct_uniq. fsetdec. + intros. destruct a as [y b0]. simpl_alist in *. destruct_uniq. assert (NE: not (y = x)). fsetdec. destruct E' as [|[z c]]. simpl_alist in H0. inversion H0. subst. contradiction. inversion H0. subst. simpl_alist in *. specialize (IHl F a0 b E' F'). destruct IHl as [E1 [E2 E3]]; auto. subst. auto. 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