proposition: Lemma length_flatten A (l : list (list A)) : length (flatten l) = list_sum (map (length (A:=A)) l).
proof: Proof. induction l; ins; desf; rewrite length_app; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation