proposition: Lemma mk_list_nth A i n f (d : A) : nth i (mk_list n f) d = if le_lt_dec n i then d else f i.
proof: Proof. induction n; ins; desf; rewrite app_nth; desf; rewrite mk_list_length in *; desf; try lia. apply nth_overflow; ins; lia. by assert (i = n) by lia; desf; rewrite minus_diag. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation