proposition: Lemma closed_many_app_nat_enc {s} ns : closed s -> closed (fold_left (fun s n => app s (nat_enc n)) ns s).
proof: Proof. elim: ns s. { done. } move=> n ns IH s ? /=. apply: IH. by apply: L_facts.app_closed; [|apply: L_facts.closed_nat_enc]. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun