Type level rewrite

Stream: general

[Kris Brown]

I can't make a MWE for this yet, but I'm in a situation where my tactic state is

ptr_eq: Π {t : TypeDecl}, decidable_eq (Ptr t)
a b: TypeDecl
x: Ptr a
y: Ptr b
hyp: a = b
⊢ decidable (x == y)

I can't use ptr_eq on x and y because Lean thinks they're different types, but by hypothesis they are not. Is there any way to rewrite y to be of type Ptr a using hyp? I've tried {simp_rw <-hyp at y, dedup} which produces a new element y_1: Ptr a but I can't make the connection between y and y_1 in that case.

[Floris van Doorn]

you can do subst hyp to turn all bs into as.

[Kris Brown]

Thanks, that worked perfectly !