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