proposition: Lemma stack_eq_dec (A B: stack) : {A = B} + {A <> B}.
proof: Proof. by do 2 (decide equality). Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM