proposition: Lemma in_mk_list_iff A (x: A) n f : In x (mk_list n f) <-> exists m, m < n /\ x = f m.
proof: Proof. induction n; ins; try (rewrite in_app_iff, IHn; clear IHn); desc; split; ins; desf; try lia; try (by repeat eexists; lia). destruct (eqP m n); desf; eauto. left; repeat eexists; ins; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation