case refl
a✝ : Sort u_1
a : a✝
e : a✝ = a✝
⊢ cast e a = a
a✝¹ a✝ : Sort u_1
e : a✝¹ = a✝
a : a✝¹
a' : a✝
h : HEq a a'
⊢ cast e a = a'
cases h
no goals
case refl
a✝ : Sort u_1
a : a✝
e : a✝ = a✝
⊢ cast e a = a
rfl