simp [hasType, List.all_cons]
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ (List.all (e :: l) fun x => hasType x τ) = true → hasType (nested (e :: l)) τ = true
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ hasType e τ = true →
    (∀ (x : TensorElem), x ∈ l → hasType x τ = true) → hasType e τ = true ∧ hasType (nested l) τ = true