case cons =>
  intros head tail motive_1 IH2 s Hshape1 Hshape2 Htype1
  simp [List.map, List.join]
  rw [Nat.add_comm]
  simp [Nat.succ_eq_add_one, Nat.right_distrib]
  simp [List.all_cons] at Hshape1
  simp [List.all_cons] at Htype1
  sorry
τ : 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
no goals