case cons head _ ih =>
  cases head <;> simp <;> apply ih
head : Dimension
tail✝ : List Dimension
ih : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head :: tail✝)) (head :: tail✝) = true
no goals