case bool =>
  constructor;
  intros s;
  intros Hshape;
  intros Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
  sorry
τ : MLIRTy
⊢ (∀ (s : List ℕ),
      hasShape (bool false) s = true →
        ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s) ∧
    ∀ (s : List ℕ),
      hasShape (bool true) s = true →
        ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
no goals