proposition: Lemma enum_states_reachable {X Y: config} : reachable M X Y -> X = Y \/ (In (get_state X) (enum_states M) /\ In (get_state Y) (enum_states M)).
proof: Proof. elim. - move=> ? ? /enum_states_step ?. by right. - move=> ?. by left. - move=> > _ + _. case. + move=> ->. case; [move=> ->; by left | move=> ?; by right]. + move=> [? ?]. case; [move=> <- | move=> [? ?]]; by right. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM