proposition: Corollary equiv_appR {x x': state} {A B A' B': stack} {b: bool} : equiv (A, B, x) (A', B', x') -> equiv (A, B ++ [b], x) (A', B' ++ [b], x').
proof: Proof. move /(equiv_app (C := []) (D := [b])). by rewrite ? app_nil_r. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM