simp [hasShape, motive_2 _ H'.2]
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
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
H' : List.length l = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ hasShape (nested l) (List.length l :: s_tail) = true
no goals