Non-dependent exists

Stream: Is there code for X?

[Marcus Rossel]

Does such a theorem exist somewhere?

example : (∃ _ : p, q) ↔ p ∧ q where
  mp  := fun ⟨hp, hq⟩ => ⟨hp, hq⟩
  mpr := fun ⟨hp, hq⟩ => ⟨hp, hq⟩

[Kyle Miller]

example : (∃ _ : p, q) ↔ p ∧ q := by
  exact? -- Try this: exact exists_prop

[Marcus Rossel]

Huh, I thought I tried that. Thanks!