proposition: Lemma mk_listE n A (f: nat -> A) : mk_list n f = map f (seq 0 n).
proof: Proof. induction n; ins; rewrite IHn. rewrite seq_split with (x:=n) (y:=S n); try lia. by rewrite map_app, plus_0_r, <- minus_Sn_m, minus_diag. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation