proposition: Lemma tab_map X Y (f: nat -> X) (g: X -> Y) k: map g (tab f k) = tab (fun x => g (f x)) k.
proof: Proof. induction k; cbn; eauto; lsimpl; now rewrite IHk. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)