proposition: Lemma UNPACK_spec' {X Y v offset} : vec_pos v X = 0 -> (offset, UNPACK X Y offset) // (offset, v) ->> (0, v).
proof: Proof. move=> H'X. apply: (concat_sss_compute_trans 0). { by apply: JZ_spec. } rewrite H'X. by apply: sss_compute_refl. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun