dependent products and equality

Stream: lean4

[David Renshaw]

Is there an easy way to prove bar below?

structure Foo (t1 : Type) (p : t1 → Prop) where
  (a : t1)
  (b : p a)

lemma bar
  (t1 : Type)
  (p : t1 → Prop)
  (x y : t1)
  (hab : x = y)
  (px : p x)
  (py : p y) : Foo.mk x px = Foo.mk y py := sorry

In Lean 3, the congr' tactic works, but I have been unable to find anything like that in Lean 4.

[Kyle Miller]

by cases hab; rfl works here. (You can do subst x instead of cases hab if you want.)

[Kyle Miller]

or by simp [hab]

[David Renshaw]

thanks!