proposition: Lemma cards_subset x1 : x1 <<= Sigma -> cards x1 <<= P.
proof: Proof. induction x1. - firstorder. - intros. intros [] []. + inv H0. unfold P. do 3 (apply in_app_iff; right). apply in_map_iff. eauto. + eapply IHx1; firstorder. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions Undecidability.Synthetic.Definitions