case cons head tail ih =>
  cases head <;> simp at *; apply (ih h)
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
no goals