proposition: Theorem reduction_deduction phi : deduction_binZF phi <-> deduction_binFST (ZF_to_FST phi).
proof: Proof. split; intros H. - repeat apply II. apply (prv_cut H). intros psi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]. all: unfold binFST; apply Ctx; intuition auto 7. - unfold ZF_to_FST in H. repeat setoid_rewrite imps in H. apply (prv_cut H). intros psi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]; trivial. 8: apply bZF_adj. all: unfold binZF; apply Ctx; intuition auto 7. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Semantics.Tarski.FullSoundness Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Reductions.PCPb_to_binZF Undecidability.FOL.ZF Undecidability.FOL.FST Undecidability.FOL.Sets(Models.FST_model Models.ZF_model binFST binZF) Lia Undecidability(Shared.ListAutomation)