proposition: Lemma tabulate_ext {X} k f1 f2 : (forall i, f1 i = f2 i :> X) -> tabulate (n := k) f1 = tabulate f2.
proof: Proof. intros H. induction k in f1, f2, H |- *; cbn. - reflexivity. - f_equal; eauto. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List