proposition: Lemma PACK_len_spec A X Y offset : length (PACK A X Y offset) = PACK_len.
proof: Proof. done. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun