cases H'
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
⊢ hasShape (nested l) s = true
case intro
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
w✝ : List ℕ
h✝ : s = List.length l :: w✝
⊢ hasShape (nested l) s = true