proposition: Lemma NoDup_map_middle : forall A B (f : A -> B) x ls2 ls1 x' ls2', NoDup (map f (ls1 ++ x :: ls2)) -> forall ls1', ls1 ++ x :: ls2 = ls1' ++ x' :: ls2' -> f x = f x' -> ls1 = ls1' /\ ls2 = ls2'.
proof: Proof. induction ls1; simpl; inversion_clear 1; intros. destruct ls1'; simpl in *. intuition congruence. injection H; clear H; intros; subst. exfalso; apply H0. autorewrite with core; simpl. rewrite H2. eapply in_or_app; simpl; eauto. destruct ls1'; simpl in *. injection H; clear H; intros; subst. rewrite <- H2 in H0. exfalso; apply H0. autorewrite with core; simpl. eapply in_or_app; simpl; eauto. injection H; clear H; intros; subst. apply IHls1 in H; eauto. intuition congruence. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)