#check epsilon -- Error

noncomputable def foo1 (f g : Nat → Nat) : Nat :=
  if f = g then 1 else 2 -- Error

section
open Classical

#check epsilon

noncomputable def foo2 (f g : Nat → Nat) : Nat :=
  if f = g then 1 else 2 -- Ok
end

#check epsilon -- Error

section

open scoped Classical
#check epsilon -- Error

noncomputable def foo3 (f g : Nat → Nat) : Nat :=
  if f = g then 1 else 2 -- Ok

end