proposition: Lemma in_split_perm A (x : A) l (IN: In x l) : exists l', Permutation l (x :: l').
proof: Proof. induction l; ins; intuition; desf; eauto. exists (a :: l'); rewrite H0; vauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation