proposition: Lemma binZF_binFOL_prv_intu : deduction_binZF ⪯ binFOL_prv_intu.
proof: Proof. exists (impl binZF). intros phi. unfold binFOL_prv_intu, deduction_binZF. setoid_rewrite <- impl_prv. rewrite List.app_nil_r. split; intros H; apply (Weak H); unfold List.incl; apply List.in_rev. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.PCP.PCP_undec Undecidability.FOL(binZF_undec FOL) Undecidability.FOL.Sets(binZF) Undecidability.FOL.ZF Undecidability.FOL.Syntax.Core Undecidability.FOL.Syntax.BinSig Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts