simp [flatten, mapWithType, List.join, ih]
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
ih : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)
no goals