case mk
α : Sort u_1
β : α → Sort u_2
x₁ : PSigma β
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝, snd := snd✝ }.fst = x₁.fst
h₁ : HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
⊢ { fst := fst✝, snd := snd✝ } = x₁
α : Sort u_1
β : α → Sort u_2
x₀ x₁ : PSigma β
h₀ : x₀.fst = x₁.fst
h₁ : HEq x₀.snd x₁.snd
⊢ x₀ = x₁
cases x₀
case mk.mk
α : Sort u_1
β : α → Sort u_2
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₁ : HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
case mk
α : Sort u_1
β : α → Sort u_2
x₁ : PSigma β
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝, snd := snd✝ }.fst = x₁.fst
h₁ : HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
⊢ { fst := fst✝, snd := snd✝ } = x₁
cases x₁
case mk.mk.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝¹ snd✝ : β fst✝
h₁ : HEq { fst := fst✝, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
case mk.mk
α : Sort u_1
β : α → Sort u_2
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₁ : HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
cases h₀
case mk.mk.refl.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
case mk.mk.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝¹ snd✝ : β fst✝
h₁ : HEq { fst := fst✝, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
cases h₁
no goals
case mk.mk.refl.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
rfl