proposition: Lemma sym_word_R R u v : (u, v) el R -> v <<= sym R.
proof: Proof. induction R; cbn; intros. - tauto. - destruct a as (u', v'). destruct H. + inv H. intros x Hx. rewrite ? in_app_iff. right. now left. + intros x Hx. rewrite ? in_app_iff. right. right. now eapply IHR. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)