diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,10 @@
+2025-03-07
+        * Version bump (4.3). (#604)
+        * Fix typo in documentation. (#587)
+        * Record how a Property's underlying proposition is quantified. (#254)
+        * Remove deprecated function Copilot.Language.Operators.Array.(.!!).
+          (#599)
+
 2025-01-07
         * Version bump (4.2). (#577)
         * Bump upper version constraint on containers. (#570)
diff --git a/copilot-language.cabal b/copilot-language.cabal
--- a/copilot-language.cabal
+++ b/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             4.2
+version:             4.3
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -42,9 +42,9 @@
                , data-reify            >= 0.6  && < 0.7
                , mtl                   >= 2.0  && < 3
 
-               , copilot-core          >= 4.2 && < 4.3
-               , copilot-interpreter   >= 4.2 && < 4.3
-               , copilot-theorem       >= 4.2 && < 4.3
+               , copilot-core          >= 4.3 && < 4.4
+               , copilot-interpreter   >= 4.3 && < 4.4
+               , copilot-theorem       >= 4.3 && < 4.4
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/src/Copilot/Language/Analyze.hs b/src/Copilot/Language/Analyze.hs
--- a/src/Copilot/Language/Analyze.hs
+++ b/src/Copilot/Language/Analyze.hs
@@ -110,7 +110,11 @@
 --
 -- This function can fail with one of the exceptions in 'AnalyzeException'.
 analyzeProperty :: IORef Env -> Property -> IO ()
-analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e
+analyzeProperty refStreams (Property _ p) =
+  -- Soundness note: it is OK to call `extractProp` here to drop the quantifier
+  -- from the proposition `p`, as the analysis does not depend on what the
+  -- quantifier is.
+  analyzeExpr refStreams (extractProp p)
 
 data SeenExtern = NoExtern
                 | SeenFun
@@ -291,7 +295,12 @@
           env' args
 
   propertyExts :: ExternEnv -> Property -> IO ExternEnv
-  propertyExts env (Property _ stream) = collectExts refStreams stream env
+  propertyExts env (Property _ p) =
+    -- Soundness note: it is OK to call `extractProp` here to drop the
+    -- quantifier from the proposition `p`. This is because we are simply
+    -- gathering externs from `p`, and the presence of externs does not depend
+    -- on what the quantifier is.
+    collectExts refStreams (extractProp p) env
 
   theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv
   theoremExts env (p, _) = propertyExts env p
diff --git a/src/Copilot/Language/Operators/Array.hs b/src/Copilot/Language/Operators/Array.hs
--- a/src/Copilot/Language/Operators/Array.hs
+++ b/src/Copilot/Language/Operators/Array.hs
@@ -8,8 +8,7 @@
 
 -- | Combinators to deal with streams carrying arrays.
 module Copilot.Language.Operators.Array
-  ( (.!!)
-  , (!)
+  ( (!)
   , (!!)
   , (=:)
   , (=$)
@@ -33,18 +32,6 @@
 (!) :: (KnownNat n, Typed t)
     => Stream (Array n t) -> Stream Word32 -> Stream t
 arr ! n = Op2 (Index typeOf) arr n
-
--- | Create a stream that carries an element of an array in another stream.
---
--- This function implements a projection of the element of an array at a given
--- position, over time. For example, if @s@ is a stream of type @Stream (Array
--- '5 Word8)@, then @s .!! 3@ has type @Stream Word8@ and contains the 3rd
--- element (starting from zero) of the arrays in @s@ at any point in time.
-{-# DEPRECATED (.!!) "This function is deprecated in Copilot 4. Use (!)." #-}
-(.!!) :: ( KnownNat n
-         , Typed t
-         ) => Stream (Array n t) -> Stream Word32 -> Stream t
-(.!!) = (!)
 
 -- | Pair a stream with an element accessor, without applying it to obtain the
 -- value of the element.
diff --git a/src/Copilot/Language/Operators/Projection.hs b/src/Copilot/Language/Operators/Projection.hs
--- a/src/Copilot/Language/Operators/Projection.hs
+++ b/src/Copilot/Language/Operators/Projection.hs
@@ -23,7 +23,7 @@
 -- | Common interface to manipulate portions of a larger data structure.
 --
 -- A projectable d s t means that it is possible to manipulate a sub-element s
--- of type t carried in a stream of type d..
+-- of type t carried in a stream of type d.
 class Projectable d s t | d s -> t where
 
   -- | Unapplied projection or element access on a type.
diff --git a/src/Copilot/Language/Reify.hs b/src/Copilot/Language/Reify.hs
--- a/src/Copilot/Language/Reify.hs
+++ b/src/Copilot/Language/Reify.hs
@@ -4,6 +4,7 @@
 -- specification.
 
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE Rank2Types                #-}
 {-# LANGUAGE Safe                      #-}
 
@@ -105,11 +106,22 @@
   -> IORef [Core.Stream]
   -> Property
   -> IO Core.Property
-mkProperty refMkId refStreams refMap (Property name guard) = do
-  w1 <- mkExpr refMkId refStreams refMap guard
+mkProperty refMkId refStreams refMap (Property name p) = do
+  p' <- mkProp refMkId refStreams refMap p
   return Core.Property
     { Core.propertyName  = name
-    , Core.propertyExpr  = w1 }
+    , Core.propertyProp  = p' }
+
+-- | Transform a Copilot proposition into a Copilot Core proposition.
+mkProp :: IORef Int
+       -> IORef (Map Core.Id)
+       -> IORef [Core.Stream]
+       -> Prop a
+       -> IO Core.Prop
+mkProp refMkId refStreams refMap prop =
+  case prop of
+    Forall e -> Core.Forall <$> mkExpr refMkId refStreams refMap e
+    Exists e -> Core.Exists <$> mkExpr refMkId refStreams refMap e
 
 -- | Transform a Copilot stream expression into a Copilot Core expression.
 {-# INLINE mkExpr #-}
diff --git a/src/Copilot/Language/Spec.hs b/src/Copilot/Language/Spec.hs
--- a/src/Copilot/Language/Spec.hs
+++ b/src/Copilot/Language/Spec.hs
@@ -153,7 +153,7 @@
 -- | A property, representing a boolean stream that is existentially or
 -- universally quantified over time.
 data Property where
-  Property :: String -> Stream Bool -> Property
+  Property :: String -> Prop a -> Property
 
 -- | A proposition, representing the quantification of a boolean streams over
 -- time.
@@ -170,6 +170,12 @@
 exists = Exists
 
 -- | 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 a -> Stream Bool
 extractProp (Forall p) = p
 extractProp (Exists p) = p
@@ -180,7 +186,7 @@
 -- This function returns, in the monadic context, a reference to the
 -- proposition.
 prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
-prop name e = tell [PropertyItem $ Property name (extractProp e)]
+prop name e = tell [PropertyItem $ Property name e]
   >> return (PropRef name)
 
 -- | A theorem, or proposition together with a proof.
@@ -188,7 +194,7 @@
 -- This function returns, in the monadic context, a reference to the
 -- proposition.
 theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
-theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]
+theorem name e (Proof p) = tell [TheoremItem (Property name e, p)]
   >> return (PropRef name)
 
 -- | Construct a function argument from a stream.