proposition: Lemma spaceP {X Y: config} : In (get_state X) (enum_states M) -> width X = width Y -> In X (space Y).
proof: Proof. rewrite /space. case: X => [[A B] x]. move=> HX <-. right. apply /in_flat_map. exists (length A). constructor=> /=. { apply /in_seq. by lia. } have -> : (length A + length B - length A = length B) by lia. by apply: enum_configsP. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM