case refl
F : Sort u_3
α : Sort u_1
β : α → Sort u_2
i : FunLike F α β
f : F
⊢ ↑f = ↑f
F : Sort u_3
α : Sort u_1
β : α → Sort u_2
i : FunLike F α β
f g : F
h : f = g
⊢ ↑f = ↑g
cases h
no goals
case refl
F : Sort u_3
α : Sort u_1
β : α → Sort u_2
i : FunLike F α β
f : F
⊢ ↑f = ↑f
rfl