proposition: Lemma tab_plus X (f: nat -> X) n m: tab f (n + m) = tab f n ++ tab (fun k => f (n + k)) m.
proof: Proof. induction n in f |-*; eauto. cbn [plus]; now rewrite tab_S, IHn, tab_S. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)