proposition: Lemma enum_stacksP {A: stack} : In A (enum_stacks (length A)).
proof: Proof. elim: A => /=; first by left. move=> a A IH. rewrite in_app_iff ? in_map_iff. case: a; [left | right]; exists A; by constructor. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM