intros head tail motive_1 ih s H
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
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
ih :
  ∀ (s : List ℕ),
    (List.all tail fun x => decide (inferredShape x = some s)) = true → (List.all tail fun x => hasShape x s) = true
s : List ℕ
H : (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true
⊢ (List.all (head :: tail) fun x => hasShape x s) = true