proposition: Lemma instr_at' mm2i p : mm2_instr_at mm2i p M -> mm2_instr_at (shift_instr mm2i) (p+a0+b0) M'.
proof: Proof. move=> /[dup] /mm2_instr_at_pos -> /nth_error_Some_mm2_instr_at_iff Hp /=. apply /nth_error_Some_mm2_instr_at_iff. rewrite /M'. rewrite nth_error_app2 repeat_length. { lia. } rewrite nth_error_app2 repeat_length. { lia. } have -> : Nat.pred p + a0 + b0 - a0 - b0 = Nat.pred p by lia. by rewrite nth_error_map Hp. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun