proposition: Lemma uniq_align_eq : forall E' F', uniq (E ++ x ~ a ++ F) -> E ++ x ~ a ++ F = E' ++ F' -> (exists E1 E2, E' = E1 ++ x ~ a ++ E2 /\ E = E1 /\ F = E2 ++ F') \/ (exists F1 F2, F' = F1 ++ x ~ a ++ F2 /\ E = E' ++ F1 /\ F = F2).
proof: Proof. clear. intros E' F' U Eq. assert (HB: binds x a (E' ++ F')). { rewrite <- Eq. auto. } rewrite -> binds_app_iff in HB. destruct HB as [h1|h1]. + left. destruct (binds_split _ _ _ _ h1) as [G0'' [E1 E2]]. eexists. eexists. split. eauto. subst. simpl_alist in Eq. edestruct (uniq_mid _ _ _ U Eq); eauto. tauto. + right. destruct (binds_split _ _ _ _ h1) as [G0'' [G0' E2]]. eexists. eexists. split. eauto. subst. rewrite <- (app_assoc _ E') in Eq. edestruct (uniq_mid _ _ _ U Eq); eauto. tauto. 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