proposition: Theorem reduction_entailment phi : entailment_binZF phi <-> entailment_binFST (ZF_to_FST phi).
proof: Proof. split; intros Hp D I rho HI. - unfold ZF_to_FST. intros H1 H2 H3 H4. apply Hp. intros psi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]; trivial. all: apply HI; unfold binFST; intuition. - apply Hp; fold sat. 2-5: apply HI; unfold binZF; intuition auto 7. intros psi [<-|[<-|[<-|[<-|[]]]]]. 1-3: apply HI; unfold binZF; intuition. apply (soundness bZF_adj). apply HI. 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)