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