i.e. Is it possible to define

example {α β : Type} (hab : α = β) (x : α) : β := sorry

From what I understand Eq.subst a b has type ∀ {α : Sort u} {motive : α → Prop} {a b : α}, a = b → motive a → motive b, but the restriction that motive must return Prop seems an unnecessary restriction and hence does not suit my need very well.

CodePudding user response：

In Lean 3 it is called eq.rec/eq.rec_on. I guess, in Lean 4 it is called Eq.rec/Eq.rec_on.

CodePudding user response：

This is Eq.cast in Lean 4.

Eq.cast : {α β : Sort u_1} → α = β → α → β