proposition: Lemma NoDup_app_unique : forall A x (ls : list A), NoDup ls -> forall ls1 ls2 ls1' ls2', ls = ls1 ++ x :: ls2 -> ls = ls1' ++ x :: ls2' -> ls1 = ls1' /\ ls2 = ls2'.
proof: Proof. induction 1; t; try length_contra; repeat match goal with | [ H : _ :: _ = _ :: _ |- _ ] => inversion H; clear H; subst | [ H : _ :: _ = ?ls ++ _ |- _ ] => destruct ls; t | [ H : _ -> False |- _ ] => exfalso; apply H; solve [ eauto using in_eq, in_or_app ] | [ H : _ |- _ ] => specialize (IHNoDup _ _ _ _ eq_refl H); intuition congruence end; auto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)