proposition: Theorem reduction_deduction phi : deduction_ZF' phi <-> deduction_HF (add_om phi).
proof: Proof. unfold deduction_ZF', deduction_HF, add_om. rewrite !imps. split; intros H; apply (Weak H); unfold ZFeq', HFeq, ZF', HF; firstorder. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF) Undecidability.FOL.ZF Lia Undecidability(Shared.ListAutomation)