proposition: Lemma reachable_stack_app {M l r x l' r' y v w} : reachable M (l, r, x) (l', r', y) -> reachable M (l ++ v, r ++ w, x) (l' ++ v, r' ++ w, y).
proof: Proof. move /reachable_to_reachable_n => [?] /reachable_n_stack_app ?. by apply: reachable_n_to_reachable. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun