proposition: Lemma IB_F rho : rho ⊨ F -> dPCPb R.
proof: Proof. intros H. unfold F in H. rewrite !impl_sat in H. eapply H. - eapply IB_F1. - eapply IB_F2. - apply IB_F3. 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.PCP.Reductions.PCPb_iff_dPCPb Undecidability(Shared.ListAutomation)