proposition: Lemma rew_app_inv (R1 R2 : SR.SRS nat) x y : SR.rew (R1 ++ R2) x y <-> SR.rew R1 x y \/ SR.rew R2 x y.
proof: Proof. split. - inversion 1 as [x0 y0 u v H0]; subst; eapply in_app_iff in H0 as [H0 | H0]. + left. econstructor. eauto. + right. econstructor. eauto. - intros [H | H]; eapply rew_subset; eauto with list. Qed.
imports: Undecidability.StringRewriting.SR Setoid List Lia