proposition: Lemma equiv_dec (X Y: config) : decidable (equiv X Y).
proof: Proof. case: (Exists_dec (fun Z => reachable M X Z /\ reachable M Y Z) (space X)). - move=> Z. case: (reachable_dec X Z) => ?; case: (reachable_dec Y Z) => ?; by firstorder done. - move=> + /ltac:(left). rewrite Exists_exists. move=> [Z [? ?]]. eexists. by eassumption. - move=> + /ltac:(right) => + [Z [? ?]]. apply. rewrite Exists_exists. exists Z. constructor; [by apply: spaceP0 | by constructor]. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM