Exists.fst

Stream: mathlib4

[Pan Lin]

Hi. In Mathlib.Logic.Basic, it confuses me:

theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
  | ⟨h, _⟩ => h
#align Exists.fst Exists.fst

theorem Exists.snd {b : Prop} {p : b → Prop} : ∀ h : Exists p, p h.fst
  | ⟨_, h⟩ => h
#align Exists.snd Exists.snd

Why Exists.fst and Exists.snd use {b : Prop} instead {b : Type*} or just {β}

[Notification Bot]

A message was moved here from #mathlib4 > Jordan Algebras by Hans Lin.

[Eric Wieser]

b : Type* would give an error here

[Yaël Dillies]

Think about what would happen if Exists.fst {b : Sort*} {p : b → Prop} : Exists p → b and you proved ∃ n : Nat, n = n using both Exists.mk 0 rfl and Exists.mk 37 rfl