src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Wed Apr 10 13:34:55 2019 +0100
@@ -43,6 +43,11 @@
 
 subsection \<open>Hilbert's Epsilon-operator\<close>
 
+lemma Eps_cong:
+  assumes "\<And>x. P x = Q x"
+  shows "Eps P = Eps Q"
+  using ext[of P Q, OF assms] by simp
+
 text \<open>
   Easier to apply than \<open>someI\<close> if the witness comes from an
   existential formula.