Require Import List Relation_Operators.
Definition Ssts := list ((nat * nat) * (nat * nat)).
Inductive step (ssts: Ssts) : list nat -> list nat -> Prop :=
| step_intro {u v: list nat} {a b c d: nat} :
In ((a, b), (c, d)) ssts -> step ssts (u ++ a :: b :: v) (u ++ c :: d :: v).
Definition multi_step (ssts: Ssts) : list nat -> list nat -> Prop :=
clos_refl_trans (list nat) (step ssts).
Definition SSTS01 : Ssts -> Prop :=
fun ssts => exists n, multi_step ssts (repeat 0 (1+n)) (repeat 1 (1+n)).