proposition: Lemma disjoint_one_l A (a : A) (l : list A) : disjoint (a :: nil) l <-> ~ In a l.
proof: Proof. unfold disjoint; intuition; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation