proposition: Theorem pcp_induction l m : P l m.
proof: Proof. Proof using IHP. induction on l m as IH with measure (length l + length m). apply IHP. intros l' m' (x & y & H & -> & ->). apply IH. do 2 rewrite app_length. destruct x; destruct y; simpl; try lia. destruct H as [ [] | [] ]; auto. 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)