proposition: Lemma NoDup_eq_simpl A l1 (a : A) l1' l2 l2' (ND : NoDup (l1 ++ a :: l1')) (L : l1 ++ a :: l1' = l2 ++ a :: l2') : l1 = l2 /\ l1' = l2'.
proof: Proof. revert l2 L; induction l1; ins; destruct l2; ins; desf. by exfalso; inv ND; eauto using in_or_app, in_eq, in_cons. by exfalso; inv ND; eauto using in_or_app, in_eq, in_cons. inv ND; eapply IHl1 in H0; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation