proposition: Lemma steps_reaches {k x y} : steps k x = Some y -> reaches x y.
proof: Proof. elim: k x. { move=> ? [<-]. by apply: rt_refl. } move=> k IH x /=. case: (mm2_sig_step_dec M x) => [[z]|]; last done. move=> ? /IH. apply: rt_trans. by apply: rt_step. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun