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