proposition: Lemma binZF_binFOL_valid : entailment_binZF ⪯ binFOL_valid.
proof: Proof. exists (impl binZF). intros phi. unfold binFOL_valid, valid, entailment_binZF. setoid_rewrite impl_sat. reflexivity. 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