proposition: Lemma drv_val domain (I : interp domain) rho u v : derivable R u v -> rho ⊨ (F1 ==> F2 ==> Pr (enc u) (enc v)).
proof: Proof. rewrite !impl_sat. intros. induction H. - eapply H0. eapply in_map_iff. exists (x/y). eauto. - eapply (H1 (∀ ∀ Pr $1 $0 → Pr (prep x $1) (prep y $0))) in IHderivable. + cbn in *. unfold enc in *. rewrite !iprep_eval in *. cbn in *. rewrite <- !iprep_app in IHderivable. eapply IHderivable. + eapply in_map_iff. exists (x/y). 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.PCP.Reductions.PCPb_iff_dPCPb Undecidability(Shared.ListAutomation)