proposition: Lemma sym_mono A P : A <<= P -> sym A <<= sym P.
proof: Proof. induction A as [ | (x,y) ]; cbn; intros. - firstorder. - eapply incl_app; try eapply incl_app. + eapply sym_word_l. eapply H. now left. + eapply sym_word_R. eapply H. now left. + eapply IHA. eapply cons_incl. eassumption. 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)