proposition: Lemma step'_inc_index x y : step' x = Some y -> index y = 1 + (index x).
proof: Proof. rewrite /step'. move: (index x) => [|p]; first done. case: (nth_error M p); last done. move=> []. - by move=> [<-]. - by move=> [<-]. - move: (value1 x) => [|?]; [|done]. by move=> _ [<-]. - move: (value2 x) => [|?]; [|done]. by move=> _ [<-]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun