diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # language-ats
 
+## 1.7.3.0
+
+  * Update `PrVal` to include a field for universal quantifiers
+
 ## 1.7.2.0
 
   * Update `termetric` field type to allow empty termetrics
diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version:   1.18
 name:            language-ats
-version:         1.7.2.0
+version:         1.7.3.0
 license:         BSD3
 license-file:    LICENSE
 copyright:       Copyright: (c) 2018-2019 Vanessa McHale
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -981,9 +981,9 @@
         | val Pattern eq colon {% left $ Expected $4 "Expression" ":" }
 
 StaticDeclaration :: { Declaration AlexPosn }
-                  : prval Pattern eq StaticExpression { PrVal $2 (Just $4) Nothing } -- FIXME: prval should use static expressions as well.
-                  | prval Pattern colon Type { PrVal $2 Nothing (Just $4) }
-                  | prval Pattern colon Type eq StaticExpression { PrVal $2 (Just $6) (Just $4) }
+                  : prval Universals Pattern eq StaticExpression { PrVal $2 $3 (Just $5) Nothing } -- FIXME: prval should use static expressions as well.
+                  | prval Universals Pattern colon Type { PrVal $2 $3 Nothing (Just $5) }
+                  | prval Universals Pattern colon Type eq StaticExpression { PrVal $2 $3 (Just $7) (Just $5) }
                   | prvar Pattern eq StaticExpression { PrVar $2 (Just $4) Nothing }
                   | prvar Pattern colon Type { PrVar $2 Nothing (Just $4) }
                   | prvar Pattern colon Type eq StaticExpression { PrVar $2 (Just $6) (Just $4) }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -609,9 +609,9 @@
     pretty (DataSort _ s ls)                = "datasort" <+> text s <+> "=" <$> prettyDSL (toList ls)
     pretty (Impl as i)                      = "implement" <+> prettyArgsNil as <> pretty i
     pretty (ProofImpl as i)                 = "primplmnt" <+> prettyArgsNil as <> pretty i
-    pretty (PrVal p (Just e) Nothing)       = "prval" <+> pretty p <+> "=" <+> pretty e
-    pretty (PrVal p Nothing (Just t))       = "prval" <+> pretty p <+> ":" <+> pretty t
-    pretty (PrVal p (Just e) (Just t))      = "prval" <+> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e
+    pretty (PrVal us p (Just e) Nothing)    = "prval" <> prettyUsNil us <> pretty p <+> "=" <+> pretty e
+    pretty (PrVal us p Nothing (Just t))    = "prval" <> prettyUsNil us <> pretty p <+> ":" <+> pretty t
+    pretty (PrVal us p (Just e) (Just t))   = "prval" <> prettyUsNil us <> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e
     pretty PrVal{}                          = undefined
     pretty (PrVar p (Just e) Nothing)       = "prvar" <+> pretty p <+> "=" <+> pretty e
     pretty (PrVar p Nothing (Just t))       = "prvar" <+> pretty p <+> ":" <+> pretty t
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -85,7 +85,7 @@
                    | ProofImpl { implArgs :: Args a, _impl :: Implementation a }
                    | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Maybe (Pattern a), _valExpression :: Maybe (Expression a) }
                    | StaVal [Universal a] String (Type a)
-                   | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (StaticExpression a), prValType :: Maybe (Type a) }
+                   | PrVal { valUniversals :: [Universal a], prvalPat :: Pattern a, _prValExpr :: Maybe (StaticExpression a), prValType :: Maybe (Type a) }
                    | PrVar { prvarPat :: Pattern a, _prVarExpr :: Maybe (StaticExpression a), prVarType :: Maybe (Type a) }
                    | Var { varT :: Maybe (Type a), varPat :: Pattern a, _varExpr1 :: Maybe (Expression a), _varExpr2 :: Maybe (Expression a) }
                    | AndDecl { andT :: Maybe (Type a), andPat :: Pattern a, _andExpr :: Expression a }
diff --git a/src/Language/ATS/Types/Lens.hs b/src/Language/ATS/Types/Lens.hs
--- a/src/Language/ATS/Types/Lens.hs
+++ b/src/Language/ATS/Types/Lens.hs
@@ -69,9 +69,9 @@
 valExpression _ x             = pure x
 
 prValExpr :: Traversal' (Declaration a) (Maybe (StaticExpression a))
-prValExpr f (PrVal p me mt) = (\e -> PrVal p e mt) <$> f me
-prValExpr f (PrVar p me mt) = (\e -> PrVar p e mt) <$> f me
-prValExpr _ x               = pure x
+prValExpr f (PrVal us p me mt) = (\e -> PrVal us p e mt) <$> f me
+prValExpr f (PrVar p me mt)    = (\e -> PrVar p e mt) <$> f me
+prValExpr _ x                  = pure x
 
 varExpr1 :: Traversal' (Declaration a) (Maybe (Expression a))
 varExpr1 f (Var t p e e') = (\e'' -> Var t p e'' e') <$> f e