proposition: Lemma decode_nat_nat_enc xs s n : flatten (closure xs s) = L.nat_enc n -> decode_nat xs s n.
proof: Proof. intros Hn. have := decode_nat_app_depth_r xs s. congr decode_nat. rewrite Hn. clear Hn. by elim: n => *; [|congr S]. 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