Addressed review comment on merged WebAssembly#229

Fixes the typing rule of CAUGHTadm as suggested in:
WebAssembly#229 (comment)

Author: ioannad

document/core/appendix/properties.rst

@@ -676,25 +676,28 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 * The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector.
+* The label :math:`C.\CLABELS[0]` must be defined in the context.
 
-* Under context :math:`C'`,
-  the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`.
+* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[0]`.
+  
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the first label popped from the |CLABELS| vector.
 
-* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C''` be the same :ref:`context <context>` as :math:`C'`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector.
 
-* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`.
+* Under context :math:`C''`,
+  the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`.
 
+* Then the compound instruction is valid with type :math:`[] \to [t^\ast]`.
 
 .. math::
    \frac{
      S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t_0^\ast]\to[]
      \qquad
      (val : t_0)^\ast
      \qquad
-     S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
+     S; C',\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
    }{
-     S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast]
+     S; C',\CLABELS\,(\LCATCH^?~[t^\ast]) \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast]
    }