proposition: Lemma equiv_refl {X: config} : equiv X X.
proof: Proof. exists X. constructor; by apply: rt_refl. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM