Unexpected simp_ifs behaviour

[ayhon]

While using Aeneas I ran into the following situation where I expected simp_ifs to close the goal, yet it did nothing.

theorem extracted_3 (r i : Std.Usize) (dst : Std.Slice Bool)
  (i1 : Std.Usize) (i1_post : (↑i1 : ℕ) = (↑i : ℕ) + (↑r : ℕ)) (h : i1 < dst.len)
: (if h : i.val + r.val + dst.length - (i.val + r.val) ≤ Std.Usize.max then True else False)
:= by
  simp_ifs -- Does nothing.
  have: i.val + r.val + dst.length - (i.val + r.val) ≤ Std.Usize.max := by scalar_tac
  simp only [this, reduceDIte]

I'm still able to close the goal using simp with the explicit if condition discharged by scalar_tac.

Discussion on this issue has already happened privately on Zulip.