proposition: Lemma spaceP0 {X Y: config} : reachable M X Y -> In Y (space X).
proof: Proof. move=> /[dup] [/enum_states_reachable + /reachable_width]. case. - move=> <- _. by left. - move=> [_ /spaceP] + ?. by apply. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM