case cons e l ih' =>
  simp [hasType, List.all_cons]
  intro h' h
  constructor <;> simp
  assumption
  simp[h, h']
  sorry
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType (nested (e :: l)) τ = true → (List.all (e :: l) fun x => hasType x τ) = true
no goals