case cons =>
  intros head tail motive_1 ih s H; simp [List.all_cons] at *
  simp [motive_1 _ H.1, ih _ H.2]
  sorry
e : TensorElem
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true) →
      (∀ (s : List ℕ),
          (List.all tail fun x => decide (inferredShape x = some s)) = true →
            (List.all tail fun x => hasShape x s) = true) →
        ∀ (s : List ℕ),
          (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true →
            (List.all (head :: tail) fun x => hasShape x s) = true
no goals