proposition: Lemma flatten_app A (l l' : list (list A)) : flatten (l ++ l') = flatten l ++ flatten l'.
proof: Proof. by induction l; ins; desf; ins; rewrite appA, IHl. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation