[GOAL]
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : FunLike F α β
f g : F
h : f = g
⊢ ↑f = ↑g
[PROOFSTEP]
cases h
[GOAL]
case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : FunLike F α β
f : F
⊢ ↑f = ↑f
[PROOFSTEP]
rfl
