proposition: Lemma Forall2_firstn {X Y : Type} {P : X -> Y -> Prop} {l1 l2 n} : Forall2 P l1 l2 -> Forall2 P (firstn n l1) (firstn n l2).
proof: Proof. move=> H. elim: H n. { by case=> [|?]; constructor. } move=> > ??? [|?]; by constructor. 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