proposition: Lemma nats_lt: forall k i, i ∈ nats k -> i < k.
proof: Proof. induction k; cbn; intuition idtac. lia. eapply in_map_iff in H0. destruct H0; intuition idtac; subst. specialize (IHk x H1); lia. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)