proposition: Lemma rewt_induct : forall (R : SRS) z (P : string -> Prop), (P z) -> (forall x y : string, rew R x y -> rewt R y z -> P y -> P x) -> forall s, rewt R s z -> P s.
proof: Proof. intros. induction H1; firstorder. Qed.
imports: Undecidability.StringRewriting.SR Setoid List Lia