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