proposition: Lemma equiv_app {x x': state} {A B A' B' C D: stack} : equiv (A, B, x) (A', B', x') -> equiv (A++C, B++D, x) (A'++C, B'++D, x').
proof: Proof. move=> [[[A'' B''] x''] [? ?]]. exists (A''++C, B''++D, x''). constructor; by apply: reachable_app. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM