proposition: Lemma length_compose {codes lengths offset} : Forall2 (fun c l => forall i, length (c i) = l) codes lengths -> length (compose codes offset) = list_sum lengths.
proof: Proof. move=> H. elim: H offset; [done|]. move=> c l {}codes {}lengths Hcl _ IH offset. by rewrite /= app_length Hcl IH. 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