proposition: Theorem reduction_entailment phi : entailment_ZF' phi <-> entailment_HF (add_om phi).
proof: Proof. split; intros Hp D I rho HE HI. - intros H1 H2. apply Hp; trivial. intros sigma psi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]; trivial. all: apply HI; unfold HF; intuition. - apply Hp; fold sat; trivial. 2,3: apply HI; unfold ZF'; intuition eauto 7. intros sigma psi [<-|[<-|[<-|[<-|[<-|[]]]]]]. all: apply HI; unfold ZF'; intuition. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF) Undecidability.FOL.ZF Lia Undecidability(Shared.ListAutomation)