case refl
α : Sort u_1
a : α
β : Sort u_2
y : β
⊢ (_ : a = a) ▸ y = y
α : Sort u_1
a a' : α
β : Sort u_2
y : β
h : a = a'
⊢ h ▸ y = y
cases h
no goals
case refl
α : Sort u_1
a : α
β : Sort u_2
y : β
⊢ (_ : a = a) ▸ y = y
rfl