diff --git a/lib/asl.ohm b/lib/asl.ohm
index f4ed6d1..83124de 100644
--- a/lib/asl.ohm
+++ b/lib/asl.ohm
@@ -35,9 +35,10 @@ Asl {
     FreeTextField<tag> = tag freetext 
     freetext = (~("\n" | "\r") any)+
 
-    Value = ("@v?" | "@v-"| "@v") language? value ("[" Instance "]")? ScopedField*
+    Value = ("@v?" | "@v-"| "@v") language? value ProofExample? ScopedField*
     language = "%" lower+
     value = badValue | reading
+    ProofExample = "[" Instance "]"
     badValue =  reading ("-"? reading)+
     reading = (~(space | "₀".."₉" | "ₓ" | "-") any)+ subIndex? ("⁺" | "⁻"  | "?")? modifier*
     modifier = "@" (lower | digit)+
diff --git a/lib/aslGrammar.js b/lib/aslGrammar.js
index e7f5456..b517db0 100644
--- a/lib/aslGrammar.js
+++ b/lib/aslGrammar.js
@@ -49,7 +49,7 @@ const aslSemantics = aslGrammar.createSemantics().addOperation('eval', {
   Fake: function (tag, one) {
     return {fake: true}
   },
-  Value: function (tag, language, key, openingBracket, proofExample, closingBracket, fields) {
+  Value: function (tag, language, key, proofExample, fields) {
     const ignore = /Attinger|\.\.\.|^\?$|\/.+\/|[A-Z]|^[0-9]/
     const ignoreMark = /⁻|⁺/
     const evaluatedLanguage = _.head(language.eval())
@@ -80,6 +80,9 @@ const aslSemantics = aslGrammar.createSemantics().addOperation('eval', {
       mark: mark.sourceString
     }
   },
+  ProofExample: function (openingBracket, proofExample, closingBracket) {
+    return proofExample.eval()
+  },
   badValue: function (head, dash, tail) {
     return {
       value: '?',