proposition: Lemma disjoint_rev_l A (l1 l2 : list A) : disjoint (rev l1) l2 <-> disjoint l1 l2.
proof: Proof. unfold disjoint; intuition; eapply H; eauto; try rewrite <- in_rev in *; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation