theorem Subtype.ext_iff {α : Sort u} {p : α → Prop} {a1 : { x : α // p x }} {a2 : { x : α // p x }} : a1 = a2 ↔ a1.val = a2.val

theorem Subtype.ext {α : Sort u} {p : α → Prop} {a1 : { x : α // p x }} {a2 : { x : α // p x }} : a1.val = a2.val → a1 = a2

@[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⟩