proposition: Lemma mm2_stop_index_eq {P x y} : mm2_stop P x -> index x = index y -> mm2_stop P y.
proof: Proof. move=> Hx Hxy z Hyz. move: Hyz => [i]. rewrite -Hxy => - [Hi _]. have [z' Hxz'] := mm2_progress i x. apply: Hx. eexists. by split; eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun