α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
⊢ HEq ((_ : a' = a') ▸ p) p
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
a : α
t : a' = a
⊢ HEq (t ▸ p) p
subst t
no goals
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
⊢ HEq ((_ : a' = a') ▸ p) p
rfl