case cons head tail ih =>
  cases S; simp at Hrefines
  cases head <;> simp at *
  rw [←Hrefines.1, ←ih Hknown Hrefines.2]
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ shapeProd S = prod (head :: tail)
no goals