Lemmas about Sigma from Lean 3 core.

theorem ex_of_psig {α : Sort u_1} {p : α → Prop} : (x : α) ×' p x → ∃ (x : α), p x

theorem Sigma.eq {α : Type u_1} {β : α → Type v} {p₁ : (a : α) × β a} {p₂ : (a : α) × β a} (h₁ : p₁.fst = p₂.fst) : Eq.recOn h₁ p₁.snd = p₂.snd → p₁ = p₂

theorem PSigma.eq {α : Sort u_1} {β : α → Sort v} {p₁ : (a : α) ×' β a} {p₂ : (a : α) ×' β a} (h₁ : p₁.fst = p₂.fst) : Eq.recOn h₁ p₁.snd = p₂.snd → p₁ = p₂