Add missing constraint on premises in values

spectec/doc/semantics/il/1-syntax.spectec

diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec
index d2b9df5..c493487 100644
--- a/spectec/doc/semantics/il/1-syntax.spectec
+++ b/spectec/doc/semantics/il/1-syntax.spectec
@@ -98,12 +98,12 @@
   | BOOL bool               ;; bool
   | TEXT text               ;; text
   | TUP val*                ;; ( val* )
-  | INJ typ mixop val `- quantprems?  ;; mixop val
+  | INJ typ mixop val `- quantprems?  -- if quantprems? = $trueqpr  ;; mixop val
   | OPT val?                ;; val?
   | LIST val*               ;; [ val* ]
   | STR typ valfield*       ;; { valfield* }
 
-syntax valfield = atom `= val `- quantprems?  ;; atom `=` val
+syntax valfield = atom `= val `- quantprems?  -- if quantprems? = $trueqpr  ;; atom `=` val
 
 
 syntax exp =

spectec/src/il/eval.ml

diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index 3815fd3..7231a47 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -1062,6 +1062,7 @@
 (* Subtyping *)
 
 and sub_prems _env prems1 prems2 =
+  prems2 = [] ||
   List.length prems1 = List.length prems2 &&
   List.for_all2 Eq.eq_prem prems1 prems2