proposition: Lemma nth_nats m k: m < k -> nth (nats k) m = Some m.
proof: Proof. induction k in m |-*. - lia. - intros; destruct m; cbn in *; eauto. erewrite map_nth_error; eauto. eapply IHk; lia. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)