proposition: Lemma narrow_equiv {X Y: config} : equiv X Y -> narrow X -> narrow Y.
proof: Proof. Proof using confluent_M. move=> /equiv_sym HXY [x [A HX]]. exists x, A. apply: (equiv_trans); by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM