proposition: Lemma repeated_tab (x: X) n: repeat x n = tab (Basics.const x) n.
proof: Proof. induction n; eauto; cbn [tab]. replace (S n) with (n + 1) by lia. rewrite repeated_plus; cbn. rewrite IHn; reflexivity. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)