proposition: Lemma reachable_width {X Y: config} : reachable M X Y -> width X = width Y.
proof: Proof. elim; clear. - move=> X Y. case=> *; rewrite /width /length; by lia. - done. - move=> *. by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM