proposition: Lemma In_pathI k x K : k < K -> In (steps k x) (path K x).
proof: Proof. move=> ?. apply /in_map_iff. exists k. split; first done. apply /in_seq. lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun