proposition: Lemma tab_nth {X} n m (f: nat -> X): n < m -> nth (tab f m) n = Some (f n).
proof: Proof. induction 1; cbn. + rewrite nth_error_app2, tab_length, Nat.sub_diag; cbn; eauto. rewrite tab_length; eauto. + rewrite nth_error_app1; eauto. now rewrite tab_length. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)