proposition: Lemma perm_from_subset : forall A (l : list A) l', NoDup l' -> (forall x, In x l' -> In x l) -> exists l'', Permutation l (l' ++ l'').
proof: Proof. induction l; ins; vauto. by destruct l'; ins; vauto; exfalso; eauto. destruct (classic (In a l')). eapply In_split in H1; desf; rewrite ?nodup_app, ?nodup_cons in *; desf. destruct (IHl (l1 ++ l2)); ins. by rewrite ?nodup_app, ?nodup_cons in *; desf; repeat split; ins; red; eauto using in_cons. by specialize (H0 x); rewrite in_app_iff in *; ins; desf; destruct (classic (a = x)); subst; try tauto; exfalso; eauto using in_eq. eexists; rewrite app_ass in *; ins. by eapply Permutation_trans, Permutation_middle; eauto. destruct (IHl l'); eauto; ins. by destruct (H0 x); auto; ins; subst. by eexists (a :: _); eapply Permutation_trans, Permutation_middle; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation