induction l <;> intros h
τ : MLIRTy
l : List TensorElem
⊢ ∀ (h : hasType (nested l) τ = true), flatten (nested l) h = List.join (mapWithType l flatten h)
case nil
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_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)