Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In Lean 3, simp works in the following snippet while in Lean 4 it doesn't. This is maybe due to simp using rw instead of subst internally?

example (q : p → Prop) (h : p = True)
  (h' : ∀(q : True → Prop), (∀ x, q x) ↔ q True.intro) :
    (∀ h', q h') ↔ q (h.symm ▸ trivial) := by
  simp only [h, h'] -- no change in goal in Lean 4
  -- rw [h] -- motive not type correct :-/
  subst h
  simp [h'] -- works fine now