proposition: Lemma sym_G_rewt x G y : x <<= sym_G G -> rewt G x y -> y <<= sym_G G.
proof: Proof. intros. induction H0. - eauto. - destruct H1. destruct R. cbn in *. pose (incl_app_inv _ _ IHrewt) as HH. eapply incl_app. { apply HH. } eapply incl_app. + unfold sym_G. intros ? ?. right. eapply in_flat_map. exists (a, v). eauto. + eapply incl_cons_inv, HH. Qed.
imports: Setoid Morphisms List Arith Lia Undecidability.CFG.CFP Undecidability.CFG.CFG Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions