proposition: Lemma path_loopE' K x : In (steps K x) (path K x) -> forall y, reaches x y -> In (Some y) (path K x).
proof: Proof. move=> /path_loopE H y /reaches_steps [k] H'. move: (H k). by congr In. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun