proposition: Lemma helper_closed k : bound k (Vector.fold_right (fun (n : nat) (s0 : term) => ext (@cons nat) n s0) (many_vars k) (ext (@nil nat))).
proof: Proof. induction k. - cbn. cbv. repeat econstructor. - rewrite many_vars_S. cbn. econstructor. 1: econstructor. 1: eapply closed_dcl_x. 1: Lproc. 1: econstructor; lia. eapply bound_ge. 1: eauto. lia. 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)