induction S <;> simp
S : List ℕ
⊢ shapeRefines S (List.map Dimension.Known S) = true
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
⊢ shapeRefines tail✝ (List.map Dimension.Known tail✝) = true