proposition: Lemma nth_error_Some_mm2_instr_at_iff {P: list mm2_instr} i instr : nth_error P i = Some instr <-> mm2_instr_at instr (S i) P.
proof: Proof. split. - move=> /(@nth_error_split mm2_instr) [?] [?] [-> <-]. by do 2 eexists. - move=> [?] [?] [-> [<-]]. by rewrite nth_error_app2 ?Nat.sub_diag. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun