proposition: Lemma step'_incl x y : step' x = Some y -> step x y.
proof: Proof. rewrite /step' (mm2_state_eta x) /=. case: (index x) => [|p]; first done. case Hp: (nth_error M p) => [i|]; last done. move: Hp => /nth_error_Some_mm2_instr_at_iff. case: i => > Hi. - move=> [<-]. eexists. by split; [eassumption|constructor]. - move=> [<-]. eexists. by split; [eassumption|constructor]. - case: (value1 x) => [|a]; last done. move=> [<-]. eexists. by split; [eassumption|constructor]. - case: (value2 x) => [|b]; last done. move=> [<-]. eexists. by split; [eassumption|constructor]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun