proposition: Lemma length_enum_stacks {l: nat} : length (enum_stacks l) = Nat.pow 2 l.
proof: Proof. elim: l; first done. move=> l /=. rewrite app_length ? map_length. move=> ->. by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM