proposition: Lemma enum_statesP {x y: state} {a b: symbol} {d: dir} : In (x, y, a, b, d) M -> In x (enum_states M) /\ In y (enum_states M).
proof: Proof. elim: M x y a b d=> /=; clear; first done. move=> i M IH >. case. - move=> ->. constructor; [by left | by right; left]. - move /IH=> [? ?]. move: i=> [[[[? ?] ?] ?] ?]. constructor; right; by right. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM