proposition: Lemma drv_prv (s : peirce) u v : derivable R u v -> ctx_S ⊢ Pr (enc u) (enc v).
proof: Proof. induction 1. - apply Ctx. right. eapply in_app_iff. right. rewrite <- in_rev. eapply in_map_iff. exists (x/y). eauto. - assert (ctx_S ⊢ ∀ ∀ Pr $1 $0 → Pr (prep x $1) (prep y $0)). + apply Ctx. right. eapply in_app_iff. left. rewrite <- in_rev. eapply in_map_iff. exists (x/y). eauto. + eapply AllE with (t := enc u) in H1; eauto. cbn in H1. rewrite !prep_subst in H1. cbn in H1. eapply AllE with (t := enc v) in H1; eauto. cbn in H1. unfold enc in H1. rewrite !prep_subst in H1. cbn in H1. unfold enc. rewrite !prep_app. eapply (IE H1). eassumption. 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)