proposition: Lemma equiv_trans {X Y Z: config} : equiv X Y -> equiv Y Z -> equiv X Z.
proof: Proof. Proof using confluent_M. move=> [Z0 [? HYZ0]] [Z1 [HYZ1 ?]]. have [Z2 [? ?]] := (confluent_M HYZ0 HYZ1). exists Z2. constructor; apply: rt_trans; by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM