proposition: Lemma cont_vec_correct k s (v : Vector.t nat k) : proc s -> many_app (cont_vec k s) (Vector.map enc v) == s (enc v).
proof: Proof. intros Hs. unfold cont_vec. rewrite equiv_many_app_L. 2:{ eapply beta_red. 1:Lproc. rewrite subst_many_lam. replace (k + 0) with k by lia. reflexivity. } cbn -[plus mult]. rewrite Nat.eqb_refl. rewrite bound_closed_k. 2:eapply helper_closed. replace (3 * k) with (k + 2 * k) by lia. etransitivity. { apply many_beta. eapply vector_closed. } rewrite many_subst_app. rewrite many_subst_closed. 2:Lproc. replace (2 * k) with (2 * k + 0) by lia. eapply equiv_R. induction v. - cbn. reflexivity. - rewrite many_vars_S. cbn -[mult]. rewrite subst_closed; [ | now Lproc]. rewrite Nat.eqb_refl. rewrite !many_subst_app. repeat (rewrite many_subst_closed; [ | now Lproc]). rewrite bound_closed_k. 2:eapply helper_closed. rewrite IHv. rewrite !enc_vector_eq. now Lsimpl. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability(MuRec_computable LVector) Undecidability.L.Util(NaryApp ClosedLAdmissible)