constructor
τ : 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
case left
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool false) s = true →
      ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s