proposition: Lemma rev_eq A (l l' : list A) : rev l = rev l' <-> l = l'.
proof: Proof. split; ins; desf. apply (f_equal (@rev A)) in H; rewrite !rev_rev in H; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation