@[simp]

theorem Subtype.forall {α : Sort u} {p : α → Prop} {q : { a : α // p a } → Prop} : (∀ (x : { a : α // p a }), q x) ↔ ∀ (a : α) (b : p a), q ⟨a, b⟩

@[simp]

theorem Subtype.exists {α : Sort u} {p : α → Prop} {q : { a : α // p a } → Prop} : (∃ (x : { a : α // p a }), q x) ↔ ∃ (a : α), ∃ (b : p a), q ⟨a, b⟩