Require Import Undecidability.Synthetic.Undecidability.

Require Import Undecidability.StringRewriting.SSTS.
Require Import Undecidability.CounterMachines.CM2_undec.

Require Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.

Lemma SSTS01_undec : undecidable SSTS01.
Proof.
  apply (undecidability_from_reducibility CM2_HALT_undec).
  apply CM2_HALT_to_SSTS01.reduction.
Qed.

Check SSTS01_undec.