intros head tail motive_1 IH2 s Hshape1 Hshape2 Htype1
τ : MLIRTy
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ),
        hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s) →
      (∀ (s : List ℕ),
          (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
            ∀ (h : (List.all tail fun x => hasType x τ) = true),
              List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                List.length tail * shapeProd s) →
        ∀ (s : List ℕ),
          hasShape head s = true →
            (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
              ∀ (h : (List.all (head :: tail) fun x => hasType x τ) = true),
                List.length (flatten head (_ : hasType head τ = true)) +
                    List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                  Nat.succ (List.length tail) * shapeProd s
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (flatten head (_ : hasType head τ = true)) +
      List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
    Nat.succ (List.length tail) * shapeProd s