proposition: Lemma Forall2_repeat {X Y : Type} {P : X -> Y -> Prop} {l y n} : length l = n -> Forall (fun x => P x y) l -> Forall2 P l (repeat y n).
proof: Proof. move=> + H. elim: H n. - by move=> [|n] ?; [constructor|]. - move=> > ?? IH [|n]; [done|]. move=> [/IH] ?. 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