proposition: Lemma tab_map_nats X k (f: nat -> X): tab f k = map f (nats k).
proof: Proof. induction k in f |-*; eauto. cbn [nats map]; now rewrite tab_S, IHk, map_map. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)