proposition: Theorem undecidable_deduction_binFST : undecidable deduction_binFST.
proof: Proof. apply (undecidability_from_reducibility undecidable_deduction_binZF). exists ZF_to_FST. intros phi. apply reduction_deduction. Qed.
imports: Undecidability.Synthetic(Definitions Undecidability) Undecidability.FOL(Sets.binFST Sets.binZF Sets.Models.FST_model) Undecidability.FOL.FST Undecidability.FOL(Reductions.binZF_to_binFST FST_undec binZF_undec)