proposition: Lemma equiv_sym {X Y: config} : equiv X Y <-> equiv Y X.
proof: Proof. constructor; move=> [Z [? ?]]; exists Z; by constructor. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM