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