cases head <;> simp at *
head : Dimension
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
h : known (head :: tail) = true
⊢ shapeRefines (project (head :: tail)) (head :: tail) = true
case Known
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
a✝ : ℕ
h : known tail = true
⊢ shapeRefines (project tail) tail = true