rw failed but subst worked handling List

Stream: new members

[Zhang Qinchuan]

When handling List, I failed to rw but subst worked.

import Mathlib

example (xs : List ℕ) (h : xs = [0, 1] ++ [2, 3]) [NeZero xs.length] : List.get xs 2 = 2 := by
  --rw [h]
  -- failed! with the following outputs:
  --   has type
  --   NeZero xs.length : Prop
  -- but is expected to have type
  --   NeZero _a.length : Prop

  subst h -- success!
  sorry

[Chris Wong]

Yes, subst rewrites everything, including the NeZero hypothesis, whereas rw only rewrites the goal (unless you specify other targets explicitly).