diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,9 @@
+2025-03-07
+        * Version bump (4.3). (#604)
+        * Fix typo in documentation. (#587)
+        * Add a Show instance for Type. (#589)
+        * Add a Prop type to capture how a property is quantified. (#254)
+
 2025-01-07
         * Version bump (4.2). (#577)
         * Deprecate fields of Copilot.Core.Expr.UExpr. (#565)
diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             4.2
+version:             4.3
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs
--- a/src/Copilot/Core/Spec.hs
+++ b/src/Copilot/Core/Spec.hs
@@ -13,13 +13,15 @@
 --
 -- In order to be executed, high-level Copilot Language Spec must be turned
 -- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core
--- representations for Specs and the main types of element in a spec..
+-- representations for Specs and the main types of element in a spec.
 module Copilot.Core.Spec
     ( Stream (..)
     , Observer (..)
     , Trigger (..)
     , Spec (..)
     , Property (..)
+    , Prop (..)
+    , extractProp
     )
   where
 
@@ -62,8 +64,25 @@
 -- universally quantified over time.
 data Property = Property
   { propertyName :: Name
-  , propertyExpr :: Expr Bool
+  , propertyProp :: Prop
   }
+
+-- | A proposition, representing a boolean stream that is existentially or
+-- universally quantified over time.
+data Prop
+  = Forall (Expr Bool)
+  | Exists (Expr Bool)
+
+-- | Extract the underlying stream from a quantified proposition.
+--
+-- Think carefully before using this function, as this function will remove the
+-- quantifier from a proposition. Universally quantified streams usually require
+-- separate treatment from existentially quantified ones, so carelessly using
+-- this function to remove quantifiers can result in hard-to-spot soundness
+-- bugs.
+extractProp :: Prop -> Expr Bool
+extractProp (Forall e) = e
+extractProp (Exists e) = e
 
 -- | A Copilot specification is a list of streams, together with monitors on
 -- these streams implemented as observers, triggers or properties.
diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs
--- a/src/Copilot/Core/Type.hs
+++ b/src/Copilot/Core/Type.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE KindSignatures            #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE StandaloneDeriving        #-}
 {-# LANGUAGE Trustworthy               #-}
 {-# LANGUAGE TypeApplications          #-}
 {-# LANGUAGE TypeOperators             #-}
@@ -154,6 +155,7 @@
                          , Typed t
                          ) => Type t -> Type (Array n t)
   Struct :: (Typed a, Struct a) => a -> Type a
+deriving instance Show (Type a)
 
 -- | Return the length of an array from its type
 typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int