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