proposition: Lemma NoDupOK {A : Type} : forall (l l' : list A), incl l l' -> length l = length l' -> NoDup l -> Permutation.Permutation l l'.
proof: Proof. intro l; induction l; intros l' Hincl Hlength HNoDup. simpl in Hlength. apply eq_sym in Hlength. apply lengthNilOK in Hlength. subst. apply Permutation.perm_nil. induction l'. simpl in Hlength. discriminate. clear IHl'. rename a0 into a'. assert (HIn := in_eq a l). assert (H := Hincl). unfold incl in H. apply H in HIn. clear H. apply in_split in HIn. destruct HIn as [l1 [l2 Hl']]. rewrite Hl' in *. apply Permutation.Permutation_cons_app. apply IHl. unfold incl. intros e HIn. unfold incl in Hincl. assert (H := Hincl e). clear Hincl. assert (HIn' := in_cons a e l HIn). apply H in HIn'. clear H. apply in_app_or in HIn'. elim HIn'; clear HIn'; intro HIn'. apply in_or_app. auto. apply in_inv in HIn'. elim HIn'; clear HIn'; intro HIn'. subst. assert (H := NoDup_remove_2 nil l e). simpl in H. apply H in HNoDup. contradiction. apply in_or_app. auto. rewrite app_length. rewrite app_length in Hlength. simpl in Hlength. rewrite <- plus_n_Sm in Hlength. apply eq_add_S in Hlength. assumption. assert (H := NoDup_remove_1 nil l a). simpl in H. apply H. assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality