proposition: Lemma firstn_repeat {X : Type} n {x : X} m : firstn n (repeat x m) = repeat x (Nat.min n m).
proof: Proof. elim: n m => [|n IH]. { done. } move=> [|m]; [done|]. by rewrite /= IH. 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