proposition: Lemma rewt_subset R P x y : rewt R x y -> incl R P -> rewt P x y.
proof: Proof. induction 1; intros. - reflexivity. - inversion H. subst. eapply rewS; eauto. eapply rewB. eauto. Qed.
imports: Undecidability.StringRewriting.SR Setoid List Lia