How to use Path.Homotopy.refl?

Stream: new members

[Jakub Nowak]

I have a goal like p.Homotopy q and I want to change it to p = q. There is docs#Path.Homotopy.refl and docs#Path.Homotopy.cast but what I would want to have is something like:

theorem Homotopy.refl_eq {p q : Path a b} (h : p = q) : p.Homotopy q := by
  rw [h]
  exact refl q

Is there a way to use Path.Homotopy.refl directly without this additional lemma, or should we add this lemma to mahtlib?
Here's mwe:

opaque foo : Nat → Nat → Prop

axiom foo_prop : foo n n

example : foo a b := by
  suffices a = b by subst this; exact foo_prop

[Damiano Testa]

Does convert foo_prop get close enough?

[Jakub Nowak]

Yup, thanks!