fact: Definition ax_sep' phi := ∀ ∃ ∀ $0 ∈' $1 <~> $0 ∈' $2 ∧ phi[$0.: Nat.add 3 >> var].
imports: Undecidability.FOL.Util.Syntax Undecidability.FOL.Util.FullTarski Undecidability.FOL.Util.FullDeduction Undecidability.FOL.ZF List