proposition: Lemma fun2vec_ext {n} {m} {X} (f g : nat -> X) : (forall x, f x = g x) -> fun2vec n m f = fun2vec n m g.
proof: Proof. intros E. induction m in n |- *; cbn; congruence. Qed.
imports: Lia Nat Fin Undecidability.H10.Util.Diophantine Undecidability.FRACTRAN(FRACTRAN_computable prime_seq) Undecidability.H10(fractran_dio DPRM dio_logic) Undecidability.Shared.Libs.DLW(vec)