proposition: Lemma enum_configsP (x: state) (A B: stack) : In x (enum_states M) -> In (A, B, x) (enum_configs (length A) (length B)).
proof: Proof. move=> Hx. rewrite /enum_configs ? in_prod_iff. have ? := enum_stacksP. by (constructor; first by constructor). Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM