simp [hasType]
case nil
τ : MLIRTy
⊢ (List.all [] fun x => hasType x τ) = true → hasType (nested []) τ = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : (List.all tail✝ fun x => hasType x τ) = true → hasType (nested tail✝) τ = true
⊢ (List.all (head✝ :: tail✝) fun x => hasType x τ) = true → hasType (nested (head✝ :: tail✝)) τ = true
case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : (List.all tail✝ fun x => hasType x τ) = true → hasType (nested tail✝) τ = true
⊢ (List.all (head✝ :: tail✝) fun x => hasType x τ) = true → hasType (nested (head✝ :: tail✝)) τ = true