simp [List.map]
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝