proposition: Lemma tab_ext {X} (f g: nat -> X) n: (forall x, f x = g x) -> tab f n = tab g n.
proof: Proof. rewrite !tab_map_nats. intros; now apply map_ext. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)