proposition: Lemma sym_word_R R u v : In (u / v) R -> incl v (sym R).
proof: Proof. induction R; cbn; intros. - easy. - destruct a as (u', v'). destruct H; try inversion H; subst; eauto with list. Qed.
imports: Undecidability.StringRewriting.SR Setoid List Lia