proposition: Lemma sym_map X (f : X -> card nat) l Sigma : (forall x : X, x el l -> sym [f x] <<= Sigma) -> sym (map f l) <<= Sigma.
proof: Proof. intros. induction l as [ | ]; cbn in *. - firstorder. - pose proof (H a). destruct (f a). repeat eapply incl_app. + eapply app_incl_l, H0. eauto. + eapply app_incl_l, app_incl_R; eauto. + eauto. 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)