induction D <;> simp
D : DimList
⊢ shapeRefines (defaultRefinement D) D = true
case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head✝ :: tail✝)) (head✝ :: tail✝) = true