chore: remove an unused congr lemma (#12567)

This removes a `congr` lemma which is unused in Mathlib, and on Lean `master` can trigger exponential behaviour. (edit: in fact, the remaining congr lemma here still triggers exponential behaviour, just with a smaller exponent than with both) Seems safest to just get it out of the way, and I'll separately report the linear --> exponential change on `master`, as it may affect other congr lemmas which are harder to simply remove.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Logic/Basic.lean

@@ -935,12 +935,6 @@ theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔
   ⟨fun ⟨_, _⟩ ↦ ⟨hp.1 ‹_›, (hq _).1 ‹_›⟩, fun ⟨_, _⟩ ↦ ⟨_, (hq _).2 ‹_›⟩⟩
 #align exists_prop_congr exists_prop_congr
 
-@[congr]
-theorem exists_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
-    Exists q = ∃ h : p', q' (hp.2 h) :=
-  propext (exists_prop_congr hq hp)
-#align exists_prop_congr' exists_prop_congr'
-
 /-- See `IsEmpty.exists_iff` for the `False` version. -/
 @[simp] theorem exists_true_left (p : True → Prop) : (∃ x, p x) ↔ p True.intro :=
   exists_prop_of_true _