proposition: Lemma mk_list_length A n (f : nat -> A) : length (mk_list n f) = n.
proof: Proof. induction n; ins; rewrite app_length; ins; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation