proposition: Lemma CND_BPCP : [] ⊢C (F R) -> PCPb R.
proof: Proof. intros H % Double % soundness. specialize (H _ (IB R) (fun _ => nil)). unfold F, F1, F2 in H. rewrite !impl_trans, !map_map, !impl_sat in H. cbn in H. eapply PCPb_iff_dPCPb. eapply H; try tauto. - intros ? [(x,y) [<- ?] ] % in_map_iff ?. cbn in *. eapply H1. left. now rewrite !IB_enc. - intros ? [(x,y) [<- ?] ] % in_map_iff ? ? ? ?. cbn in *. eapply H1. intros. eapply H2. rewrite !IB_prep. cbn. econstructor 2; trivial. - intros. eapply H0. intros. unfold dPCPb, dPCP. eauto. Qed.
imports: Undecidability.PCP(PCP Util.PCP_facts) Undecidability.FOL(Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Semantics.Tarski.FragmentSoundness Syntax.Core Syntax.Facts) Undecidability.FOL(FOL) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts MoreReducibilityFacts) Undecidability.FOL.Reductions.PCPb_to_FOL Undecidability.PCP.Reductions.PCPb_iff_dPCPb List Undecidability(Shared.ListAutomation)