cases s <;> simp [hasShape] at Hshape
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
s : List ℕ
Hshape : hasShape (nested l) s = true
Htype : hasType (nested l) τ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd s
case cons
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
head✝ : ℕ
tail✝ : List ℕ
Hshape : List.length l = head✝ ∧ ∀ (x : TensorElem), x ∈ l → hasShape x tail✝ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (head✝ :: tail✝)