diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,22 @@
+# language-ats 
+
+## 1.6.0.0
+
+Breaking Changes:
+
+  * Remove types for `RecordValues` and instead rely on typed expressions.
+  * Remove `Wildcard` constructor and instead treat `_` as a name
+  * Remove `ParenType` and instead use tuples
+
+Enhancements:
+
+  * Better Error messages
+  * Add support for boxed records
+  * Add support for proof expressions introducing witnesses (`[ m | [] ]`)
+
+Bug Fixes:
+
+  * Fix bug with formatting for type arguments
+  * Fix formatting for `val ... and ...` declarations
+  * Fix parse error on expressions like `list_vt_cons(x, _)`
+  * Add support for patterns using binary operators.
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.5.0.0
+version: 1.6.0.0
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
@@ -19,6 +19,7 @@
     test/data/stdlib/*.sats
     test/data/stdlib/*.out
 extra-doc-files: README.md
+                 CHANGELOG.md
 
 source-repository head
     type: darcs
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
@@ -157,6 +157,7 @@
     closeParen { Special $$ ")" }
     openParen { Special $$ "(" }
     boxTuple { Special $$ "'(" }
+    boxRecord { Special $$ "'{" }
     colon { SignatureTok $$ "" }
     signature { SignatureTok _ $$ }
     comma { Special $$ "," }
@@ -247,13 +248,18 @@
 comma_sep(p)
     : sep_by(p, comma) { $1 }
 
-between(p1,p,p2) : p1 p p2 { $2 }
+parens(p) : openParen p closeParen { $2 }
 
-parens(p) : between(openParen, p, closeParen) { $1 }
+sqbrackets(p) : lsqbracket p rsqbracket { $2 }
 
+braces(p) : lbrace p rbrace { $2 }
+
 alt(p,q) : p { $1 }
          | q { $1 }
 
+optional(p) : p { Just $1 }
+            | { Nothing }
+
 ATS : Declarations { ATS (reverse $1) }
 
 -- | Parse declarations in a list
@@ -272,7 +278,7 @@
 -- | Parse a type
 Type : Name parens(TypeInExpr) { Dependent $1 $2 }
      | Name doubleParens { Dependent $1 [] }
-     | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $ to_string $1) $3 }
+     | identifierSpace parens(TypeInExpr) { Dependent (Unqualified $ to_string $1) $2 }
      | identifierSpace { Named (Unqualified $ to_string $1) }
      | specialIdentifier string { Dependent (SpecialName (token_posn $1) (to_string $1)) [Named (Unqualified $ $2)] }
      | Name { Named $1 }
@@ -284,14 +290,12 @@
      | Name maybeProof { MaybeVal (Named $1) }
      | Type fromVT { FromVT $1 }
      | Type prfTransform Type { AsProof $1 (Just $3) }
-     | Type prfTransform underscore { AsProof $1 Nothing }
      | view at Type { ViewType $1 $3 }
      | viewPlusMinus { ViewLiteral $1 }
-     | Existential Type { Ex $1 (Just $2) }
-     | Existential { Ex $1 Nothing }
+     | Existential optional(Type) { Ex $1 $2 }
      | Universal Type { ForA $1 $2 }
      | Type at StaticExpression { AtExpr $2 $1 $3 }
-     | at lsqbracket Type rsqbracket lsqbracket StaticExpression rsqbracket { ArrayType $1 $3 $6 }
+     | at sqbrackets(Type) sqbrackets(StaticExpression) { ArrayType $1 $2 $3 }
      | atbrace Records rbrace { AnonymousRecord $1 $2 }
      | openParen TypeIn vbar TypeIn closeParen { ProofType $1 $2 $4 }
      | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }
@@ -299,7 +303,6 @@
      | openParen TypeIn closeParen lineComment { Tuple $1 (toList $2) }
      | boxTuple TypeIn closeParen { BoxTuple $1 $2 }
      | boxTuple TypeIn closeParen lineComment { BoxTuple $1 $2 }
-     | openParen Type closeParen { ParenType $1 $2 }
      | addr { AddrType $1 }
      | doubleParens { Tuple $1 mempty }
      | Type where IdentifierOr SortArgs eq Type { WhereType $2 $1 $3 $4 $6 }
@@ -323,7 +326,7 @@
         | exclamation IdentifierOr colon {% left $ OneOf $3 [",", ")"] ":" }
 
 Arg : TypeArg { $1 }
-    | StaticExpression { Arg (Second (ConcreteType $1)) } -- TODO: have some sort of stop showing bound variables that we can use to disambiguate types vs. static expressions?
+    | StaticExpression { Arg (Second (ConcreteType $1)) } -- TODO: have some sort of state showing bound variables that we can use to disambiguate types vs. static expressions?
 
 -- | Parse a literal
 Literal : uintLit { UintLit $1 }
@@ -340,7 +343,6 @@
 -- | Parse a pattern match
 Pattern : Name { PName $1 [] }
         | identifierSpace { PName (Unqualified $ to_string $1) [] }
-        | underscore { Wildcard $1 }
         | identifier doubleParens { PName (Unqualified (to_string $1 ++ "()")) [] }
         | tilde Pattern { Free $2 }
         | Name openParen PatternIn closeParen { PName $1 $3 }
@@ -374,7 +376,7 @@
 IfCase : case_pattern(Expression, Expression) { $1 }
 
 ExpressionPrf : ExpressionIn { (Nothing, $1) }
-              | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?
+              | ExpressionIn vbar ExpressionIn { (Just $1, $3) }
 
 -- | A list of comma-separated expressions
 ExpressionIn : comma_sep(Expression) { toList $1 }
@@ -404,30 +406,29 @@
 -- | Expression or named call to an expression
 Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }
            | PreExpression { $1 }
-           -- | openParen PreExpression comma PreExpression vbar PreExpression closeParen { ProofExpr $1 [$2, $4] $6 }
            | openParen comma_sep(PreExpression) vbar PreExpression closeParen { ProofExpr $1 $2 $4 }
            | Expression semicolon Expression { Precede $1 $3 }
            | Expression semicolon { $1 }
            | openParen Expression closeParen { $2 }
-           | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible?
-           | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }
+           | Expression colon Type { TypeSignature $1 $3 }
+           | list_vt braces(Type) parens(ExpressionIn) { ListLiteral $1 "vt" $2 $3 }
            | begin Expression extern {% left $ Expected $3 "end" "extern" }
            | Expression prfTransform underscore {% left $ Expected $2 "Rest of expression or declaration" ">>" }
 
-TypeArgs : lbrace alt(Type,ExprType) rbrace { [$2] }
-         | lbrace TypeInExpr rbrace { $2 }
-         | TypeArgs lbrace alt(Type,ExprType) rbrace { $3 : $1 }
-         | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls
-         | TypeArgs lbrace TypeInExpr rbrace { $3 ++ $1 }
+TypeArgs : braces(alt(Type,ExprType)) { [[$1]] }
+         | braces(TypeInExpr) { [$1] }
+         | TypeArgs braces(alt(Type,ExprType)) { [$2] : $1 }
+         | braces(doubleDot) { [[ ImplicitType $1 ]] } -- FIXME only valid on function calls
+         | TypeArgs braces(TypeInExpr) { [$2] ++ $1 }
 
 Call : Name doubleParens { Call $1 [] [] Nothing [] }
-     | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }
-     | identifierSpace openParen ExpressionPrf closeParen { Call (Unqualified $ to_string $1) [] [] (fst $3) (snd $3) }
-     | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) }
+     | Name parens(ExpressionPrf) { Call $1 [] [] (fst $2) (snd $2) }
+     | identifierSpace parens(ExpressionPrf) { Call (Unqualified $ to_string $1) [] [] (fst $2) (snd $2) }
+     | Name TypeArgs parens(ExpressionPrf) { Call $1 [] $2 (fst $3) (snd $3) }
      | Name TypeArgs doubleParens { Call $1 [] $2 Nothing [VoidLiteral $3] }
      | Name TypeArgs { Call $1 [] $2 Nothing [] }
      | Name Implicits doubleParens { Call $1 $2 [] Nothing [VoidLiteral $3] }
-     | Name Implicits openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) }
+     | Name Implicits parens(ExpressionPrf) { Call $1 $2 [] (fst $3) (snd $3) }
      | Name Implicits { Call $1 $2 [] Nothing [] }
      | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument
      | Name Implicits openParen ExpressionPrf fun {% left $ Expected $5 ")" "fun" }
@@ -449,18 +450,20 @@
                  | doubleParens { StaticVoid $1 }
                  | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 }
                  | identifierSpace { StaticVal (Unqualified $ to_string $1) }
-                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [$2] }
-                 | Name openParen StaticArgs closeParen { SCall $1 $3 }
-                 | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $ to_string $1) $3 }
+                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [$2] }
+                 | Name parens(StaticArgs) { SCall $1 [] $2 }
+                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 } -- TODO: static tuple?
                  | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }
                  | UnOp StaticExpression { SUnary $1 $2 }
-                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] }
-                 | identifier doubleParens { SCall (Unqualified $ to_string $1) [] }
-                 | let StaticDecls comment_after(in) end { SLet $1 $2 Nothing }
-                 | let StaticDecls in StaticExpression end { SLet $1 $2 (Just $4) }
-                 | openParen StaticExpression closeParen { $2 }
+                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] }
+                 | identifier TypeArgs doubleParens { SCall (Unqualified $ to_string $1) $2 [] }
+                 | identifier doubleParens { SCall (Unqualified $ to_string $1) [] [] }
+                 | let StaticDecls comment_after(in) end { SLet $1 (reverse $2) Nothing }
+                 | let StaticDecls in StaticExpression end { SLet $1 (reverse $2) (Just $4) }
+                 | parens(StaticExpression) { $1 }
                  | openParen lineComment StaticExpression closeParen { $3 }
                  | case StaticExpression of StaticCase { SCase $1 $2 $4 }
+                 | openExistential StaticExpression vbar StaticExpression rsqbracket { Witness $1 $2 $4 }
 
 -- | Parse an expression that can be called without parentheses
 PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }
@@ -487,20 +490,20 @@
               | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 }
               | addrAt PreExpression { AddrAt $1 $2 }
               | viewAt PreExpression { ViewAt $1 $2 }
-              | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }
-              | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }
+              | atbrace RecordVal rbrace { RecordValue $1 $2 }
+              | boxRecord RecordVal rbrace { RecordValue $1 $2 }
               | begin Expression end { Begin $1 $2 }
               | identifierSpace { NamedVal (Unqualified $ to_string $1) }
               | Name { NamedVal $1 }
-              | lbrace ATS rbrace { Actions $2 }
-              | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }
-              | for openParen PreExpression closeParen PreExpression { For $1 $3 $5 }
-              | whileStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $8 $9 Nothing }
-              | whileStar Universals Termetric openParen Args closeParen colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $12 $13 (Just $9) }
-              | forStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { ForStar $1 $2 (snd $3) $5 $8 $9 }
+              | braces(ATS) { Actions $1 }
+              | while parens(PreExpression) PreExpression { While $1 $2 $3 }
+              | for parens(PreExpression) PreExpression { For $1 $2 $3 }
+              | whileStar Universals Termetric parens(Args) plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $6 $7 Nothing }
+              | whileStar Universals Termetric parens(Args) colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $10 $11 (Just $7) }
+              | forStar Universals Termetric parens(Args) plainArrow Expression Expression { ForStar $1 $2 (snd $3) $4 $6 $7 }
               | lineComment PreExpression { CommentExpr (to_string $1) $2 }
-              | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }
-              | PreExpression where lbrace ATS rbrace { WhereExp $1 $4 }
+              | comma parens(identifier) { MacroVar $1 (to_string $2) }
+              | PreExpression where braces(ATS) { WhereExp $1 $3 }
               | include {% left $ Expected $1 "Expression" "include" }
               | staload {% left $ Expected (token_posn $1) "Expression" "staload" }
               | overload {% left $ Expected $1 "Expression" "overload" }
@@ -549,7 +552,7 @@
             | lsqbracket QuantifierArgs colon Sort rsqbracket { Existential $2 False (Just $4) Nothing }
             | openExistential QuantifierArgs colon Sort rsqbracket { Existential $2 True (Just $4) Nothing }
             | openExistential QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 True (Just $4) (Just $6) }
-            | lsqbracket StaticExpression rsqbracket { Existential mempty False Nothing (Just $2) }
+            | sqbrackets(StaticExpression) { Existential mempty False Nothing (Just $1) }
 
 Predicates : { [] }
            | StaticExpression { [$1] }
@@ -673,6 +676,7 @@
               | let {% left $ Expected $1 "=" "let" }
               | ifcase {% left $ Expected $1 "=" "ifcase" }
               | eq fun {% left $ Expected $2 "Expression" "=" }
+              | eq fn {% left $ Expected $2 "Expression" "=" }
               | eq lineComment fun {% left $ Expected $3 "Expression" "=" }
               | lbrace {% left $ Expected $1 "Expression" "{" }
 
@@ -784,7 +788,7 @@
         | Sort { [Anonymous $1] }
         | SortArg Comment { $1 }
 
-SortArgs : openParen SortArg closeParen { Just $2 }
+SortArgs : parens(SortArg) { Just $1 }
          | doubleParens { Just [] }
          | { Nothing }
 
@@ -809,7 +813,7 @@
          | abstype IdentifierOr SortArgs MaybeType { AbsType $1 $2 $3 $4 }
          | absvtype IdentifierOr SortArgs MaybeType { AbsViewType $1 $2 $3 $4 }
          | dataprop IdentifierOr SortArgs eq DataPropLeaves { DataProp $1 $2 $3 $5 }
-         | absprop IdentifierOr openParen Args closeParen { AbsProp $1 $2 $4 }
+         | absprop IdentifierOr parens(Args) { AbsProp $1 $2 $3 }
          | AndSort { $1 }
          | AndStadef { $1 }
          | SumDecl { $1 }
@@ -822,7 +826,7 @@
          | dataprop IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" }
 
 EitherInt : intLit { Left $1 }
-          | openParen Operator closeParen { Right $2 }
+          | parens(Operator) { Right $1 }
 
 Fixity : infixr EitherInt { RightFix $1 $2 }
        | infixl EitherInt { LeftFix $1 $2 }
@@ -861,7 +865,7 @@
 
 ValDecl : val Pattern colon Type eq PreExpression { [ Val (get_addendum $1) (Just $4) $2 $6 ] }
         | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }
-        | ValDecl and Pattern eq Expression { Val None Nothing $3 $5 : $1 }
+        | ValDecl and Pattern eq Expression { AndDecl Nothing $3 $5 : $1 }
         | extern ValDecl { over _head (Extern $1) $2 }
         | val Pattern eq colon {% left $ Expected $4 "Expression" ":" }
 
@@ -899,7 +903,7 @@
      | dynload { (False, $1) }
 
 MacroArgs : doubleParens { Just [] }
-          | openParen IdentifiersIn closeParen { Just $2 }
+          | parens(IdentifiersIn) { Just $1 }
           | { Nothing }
 
 -- | Parse a declaration
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
@@ -14,7 +14,7 @@
 
 import           Control.Composition          hiding ((&))
 import           Data.Bool                    (bool)
-import           Data.Foldable                (fold, toList)
+import           Data.Foldable                (toList)
 import           Data.Functor.Foldable        (cata)
 import           Data.List                    (isPrefixOf)
 import           Data.List.NonEmpty           (NonEmpty (..))
@@ -144,22 +144,22 @@
         a (NamedValF nam)               = pretty nam
         a (CallF nam [] [] Nothing [])  = pretty nam <> "()"
         a (CallF nam [] [] e xs)        = pretty nam <> prettyArgsProof e xs
-        a (CallF nam [] us Nothing [])  = pretty nam <> prettyArgsU "{" "}" us
+        a (CallF nam [] us Nothing [])  = pretty nam <> prettyTypes us
         a (CallF nam [] us Nothing [x])
-            | startsParens x = pretty nam <> prettyArgsU "{" "}" us <> pretty x
-        a (CallF nam [] us e xs)        = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
+            | startsParens x = pretty nam <> prettyTypes us <> pretty x
+        a (CallF nam [] us e xs)        = pretty nam <> prettyTypes us <> prettyArgsProof e xs
         a (CallF nam is [] Nothing [])  = pretty nam <> prettyImplicits is
         a (CallF nam is [] Nothing [x])
             | startsParens x = pretty nam <> prettyImplicits is <> pretty x
         a (CallF nam is [] e xs)        = pretty nam <> prettyImplicits is <> prettyArgsProof e xs
         a (CallF nam is us Nothing [x])
-            | startsParens x = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> pretty x
-        a (CallF nam is us e xs)        = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
+            | startsParens x = pretty nam <> prettyImplicits is <> prettyTypes us <> pretty x
+        a (CallF nam is us e xs)        = pretty nam <> prettyImplicits is <> prettyTypes us <> prettyArgsProof e xs
         a (CaseF _ add' e cs)           = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs)
         a (IfCaseF _ cs)                = "ifcase" <$> indent 2 (prettyIfCase cs)
         a (VoidLiteralF _)              = "()"
-        a (RecordValueF _ es Nothing)   = prettyRecord es
-        a (RecordValueF _ es (Just x))  = prettyRecord es <+> ":" <+> pretty x
+        a (RecordValueF _ es)           = prettyRecord es
+        a (BoxRecordValueF _ es)        = "'" <> prettyRecord es
         a (PrecedeF e e')               = parens (e <+> ";" </> e')
         a (PrecedeListF es)             = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")
         a (AccessF _ e n)
@@ -195,8 +195,6 @@
         a (MacroVarF _ s) = ",(" <> text s <> ")"
         a BinListF{} = undefined -- Shouldn't happen
 
-        prettyImplicits = fold . fmap (prettyArgsU "<" ">") . reverse
-
         prettyIfCase []              = mempty
         prettyIfCase [(s, l, t)]     = "|" <+> s <+> pretty l <+> t
         prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t
@@ -214,7 +212,6 @@
 
 instance Eq a => Pretty (Pattern a) where
     pretty = cata a where
-        a (WildcardF _)                = "_"
         a (PSumF s x)                  = string s <+> x
         a (PLiteralF e)                = pretty e
         a (PNameF s [])                = pretty s
@@ -254,6 +251,15 @@
 endLet Nothing  = "in end"
 endLet (Just d) = "in" <$> indent 2 d <$> "end"
 
+prettyExtras :: Pretty a => Doc -> Doc -> [[a]] -> Doc
+prettyExtras d1 d2 = foldMap (prettyArgsU d1 d2) . reverse
+
+prettyTypes :: Pretty a => [[a]] -> Doc
+prettyTypes = prettyExtras "{" "}"
+
+prettyImplicits :: Pretty a => [[a]] -> Doc
+prettyImplicits = prettyExtras "<" ">"
+
 instance Eq a => Pretty (StaticExpression a) where
     pretty = cata a where
         a (StaticValF n)            = pretty n
@@ -264,14 +270,16 @@
         a (StaticHexF h)            = text h
         a StaticVoidF{}             = "()"
         a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
-        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SCallF n [] cs)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SCallF n us cs)          = pretty n <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))
         a (SPrecedeF e e')          = e <> ";" <+> e'
         a (SUnaryF op e)            = pretty op <> e
         a (SLetF _ e e') = flatAlt
-            ("let" <$> indent 2 (pretty e) <$> endLet e')
-            ("let" <+> pretty e <$> endLet e')
+            ("let" <$> indent 2 (concatSame e) <$> endLet e')
+            ("let" <+> concatSame e <$> endLet e')
         a (SCaseF ad e sls) = "case" <> pretty ad <+> e <+> "of" <$> indent 2 (prettyCases sls)
         a (SStringF s)      = text s
+        a (WitnessF _ e e') = "#[" <+> e <+> "|" <+> e' <+> "]"
 
 instance Eq a => Pretty (Sort a) where
     pretty = cata a where
@@ -313,7 +321,6 @@
         a (ViewLiteralF c)                 = "view" <> pretty c
         a ImplicitTypeF{}                  = ".."
         a (AnonymousRecordF _ rs)          = prettyRecord rs
-        a (ParenTypeF _ t)                 = parens t
         a (WhereTypeF _ t i sa t')         = t <#> indent 2 ("where" </> pretty i <+> prettySortArgs sa <+> "=" <+> pretty t')
         a AddrTypeF{}                      = "addr"
 
@@ -362,11 +369,12 @@
     pretty (Implement _ ps is us n Nothing e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> "=" <$> indent 2 (prettyImplExpr e)
 
 isVal :: Declaration a -> Bool
-isVal Val{}   = True
-isVal Var{}   = True
-isVal PrVal{} = True
-isVal PrVar{} = True
-isVal _       = False
+isVal Val{}     = True
+isVal Var{}     = True
+isVal PrVal{}   = True
+isVal PrVar{}   = True
+isVal AndDecl{} = True
+isVal _         = False
 
 notDefine :: String -> Bool
 notDefine = not . ("#define" `isPrefixOf`)
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
@@ -153,7 +153,6 @@
             | ImplicitType a
             | ViewLiteral Addendum
             | AnonymousRecord a (NonEmpty (String, Type a))
-            | ParenType a (Type a)
             | WhereType a (Type a) String (SortArgs a) (Type a)
             | AddrType a -- ^ @addr@
             deriving (Show, Eq, Generic, NFData)
@@ -178,7 +177,6 @@
                | ImplicitTypeF a
                | ViewLiteralF Addendum
                | AnonymousRecordF a (NonEmpty (String, x))
-               | ParenTypeF a x
                | WhereTypeF a x String (SortArgs a) x
                | AddrTypeF a
                deriving (Functor)
@@ -206,7 +204,6 @@
     project (ImplicitType l)           = ImplicitTypeF l
     project (ViewLiteral a)            = ViewLiteralF a
     project (AnonymousRecord l stys)   = AnonymousRecordF l stys
-    project (ParenType l ty)           = ParenTypeF l ty
     project (WhereType l ty s sas ty') = WhereTypeF l ty s sas ty'
     project (AddrType l)               = AddrTypeF l
 
@@ -226,8 +223,7 @@
             deriving (Show, Eq, Generic, NFData)
 
 -- | A data type for patterns.
-data Pattern a = Wildcard a
-               | PName (Name a) [Pattern a]
+data Pattern a = PName (Name a) [Pattern a]
                | PSum String (Pattern a)
                | PLiteral (Expression a)
                | Guarded a (Expression a) (Pattern a)
@@ -242,8 +238,7 @@
                | BinPattern a (BinOp a) (Pattern a) (Pattern a) -- ^ For use with e.g. @::@.
                deriving (Show, Eq, Generic, NFData)
 
-data PatternF a x = WildcardF a
-                  | PNameF (Name a) [x]
+data PatternF a x = PNameF (Name a) [x]
                   | PSumF String x
                   | PLiteralF (Expression a)
                   | GuardedF a (Expression a) x
@@ -261,7 +256,6 @@
 type instance Base (Pattern a) = PatternF a
 
 instance Recursive (Pattern a) where
-    project (Wildcard a)                = WildcardF a
     project (PName x ps)                = PNameF x ps
     project (PSum x p)                  = PSumF x p
     project (PLiteral e)                = PLiteralF e
@@ -368,11 +362,12 @@
                         | SPrecede (StaticExpression a) (StaticExpression a)
                         | StaticVoid a
                         | Sif { scond :: StaticExpression a, whenTrue :: StaticExpression a, selseExpr :: StaticExpression a } -- Static if (for proofs)
-                        | SCall (Name a) [StaticExpression a]
+                        | SCall (Name a) [[Type a]] [StaticExpression a]
                         | SUnary (UnOp a) (StaticExpression a)
                         | SLet a [Declaration a] (Maybe (StaticExpression a))
                         | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)]
                         | SString String -- ^ @ext#@
+                        | Witness a (StaticExpression a) (StaticExpression a) -- ^ @#[ m | () ]@
                         deriving (Show, Eq, Generic, NFData)
 
 data StaticExpressionF a x = StaticValF (Name a)
@@ -382,11 +377,12 @@
                            | SPrecedeF x x
                            | StaticVoidF a
                            | SifF x x x
-                           | SCallF (Name a) [x]
+                           | SCallF (Name a) [[Type a]] [x]
                            | SUnaryF (UnOp a) x
                            | SLetF a [Declaration a] (Maybe x)
                            | SCaseF Addendum x [(Pattern a, LambdaType a, x)]
                            | SStringF String
+                           | WitnessF a x x
                            deriving (Functor)
 
 type instance Base (StaticExpression a) = StaticExpressionF a
@@ -399,18 +395,19 @@
     project (SPrecede x x')       = SPrecedeF x x'
     project (StaticVoid x)        = StaticVoidF x
     project (Sif e e' e'')        = SifF e e' e''
-    project (SCall n es)          = SCallF n es
+    project (SCall n ts es)       = SCallF n ts es
     project (SUnary u x)          = SUnaryF u x
     project (SLet x ds e)         = SLetF x ds e
     project (SCase a x ples)      = SCaseF a x ples
     project (SString s)           = SStringF s
+    project (Witness a e e')      = WitnessF a e e'
 
 -- | A (possibly effectful) expression.
 data Expression a = Let a (ATS a) (Maybe (Expression a))
                   | VoidLiteral a -- ^ The '()' literal representing inaction.
                   | Call { callName       :: Name a
                          , callImplicits  :: [[Type a]] -- ^ E.g. @some_function<a>@
-                         , callUniversals :: [Type a] -- ^ E.g. @some_function{a}@
+                         , callUniversals :: [[Type a]] -- ^ E.g. @some_function{a}@
                          , callProofs     :: Maybe [Expression a] -- ^ E.g. @pf@ in @call(pf | str)@.
                          , callArgs       :: [Expression a] -- ^ The actual call arguments.
                          }
@@ -443,7 +440,8 @@
                          , val   :: Expression a
                          , _arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each (('Pattern' a), ('Expression' a)) pair corresponds to a branch of the 'case' statement
                          }
-                  | RecordValue a (NonEmpty (String, Expression a)) (Maybe (Type a))
+                  | RecordValue a (NonEmpty (String, Expression a))
+                  | BoxRecordValue a (NonEmpty (String, Expression a))
                   | Precede (Expression a) (Expression a)
                   | ProofExpr a (NonEmpty (Expression a)) (Expression a)
                   | TypeSignature (Expression a) (Type a)
@@ -467,7 +465,7 @@
 
 data ExpressionF a x = LetF a (ATS a) (Maybe x)
                      | VoidLiteralF a
-                     | CallF (Name a) [[Type a]] [Type a] (Maybe [x]) [x]
+                     | CallF (Name a) [[Type a]] [[Type a]] (Maybe [x]) [x]
                      | NamedValF (Name a)
                      | ListLiteralF a String (Type a) [x]
                      | IfF x x (Maybe x)
@@ -488,7 +486,8 @@
                      | UnaryF (UnOp a) x
                      | IfCaseF a [(x, LambdaType a, x)]
                      | CaseF a Addendum x [(Pattern a, LambdaType a, x)]
-                     | RecordValueF a (NonEmpty (String, x)) (Maybe (Type a))
+                     | RecordValueF a (NonEmpty (String, x))
+                     | BoxRecordValueF a (NonEmpty (String, x))
                      | PrecedeF x x
                      | ProofExprF a (NonEmpty x) x
                      | TypeSignatureF x (Type a)
@@ -536,7 +535,8 @@
     project (Unary op e)                  = UnaryF op e
     project (IfCase l arms)               = IfCaseF l arms
     project (Case l k e arms)             = CaseF l k e arms
-    project (RecordValue l recs mty)      = RecordValueF l recs mty
+    project (RecordValue l recs)          = RecordValueF l recs
+    project (BoxRecordValue l recs)       = BoxRecordValueF l recs
     project (Precede e e')                = PrecedeF e e'
     project (ProofExpr a e e')            = ProofExprF a e e'
     project (TypeSignature e ty)          = TypeSignatureF e ty
@@ -581,7 +581,8 @@
     embed (UnaryF op e)                  = Unary op e
     embed (IfCaseF l arms)               = IfCase l arms
     embed (CaseF l k e arms)             = Case l k e arms
-    embed (RecordValueF l recs mty)      = RecordValue l recs mty
+    embed (RecordValueF l recs)          = RecordValue l recs
+    embed (BoxRecordValueF l recs)       = RecordValue l recs
     embed (PrecedeF e e')                = Precede e e'
     embed (ProofExprF a e e')            = ProofExpr a e e'
     embed (TypeSignatureF e ty)          = TypeSignature e ty
diff --git a/test/data/list_append.dats b/test/data/list_append.dats
new file mode 100644
--- /dev/null
+++ b/test/data/list_append.dats
@@ -0,0 +1,47 @@
+fun
+{a:t@ype}
+list_append
+  {m,n:nat} (
+  xs: list (a, m)
+, ys: list (a, n)
+) : list (a, m+n) =
+(
+case+ xs of
+| list_cons
+    (x, xs) => list_cons (x, list_append (xs, ys))
+| list_nil ((*void*)) => ys
+) // end of [list_append]
+
+fun
+{a:t@ype}
+list_append2
+  {m,n:nat} (
+  xs: list (a, m)
+, ys: list (a, n)
+) : list (a, m+n) = let
+//
+fun loop{m:nat}
+(
+  xs: list (a, m)
+, ys: list (a, n)
+, res: &ptr? >> list (a, m+n)
+) : void =
+(
+case+ xs of
+| list_cons
+    (x, xs1) => let
+    val () = res := list_cons{a}{0}(x, _)
+    val+list_cons (_, res1) = res
+    val () = loop (xs1, ys, res1) // of [xs1] and [ys]
+  in
+    fold@(res)
+  end
+| list_nil ((*void*)) => res := ys
+)
+//
+var res: ptr
+val () = loop (xs, ys, res)
+//
+in
+  res
+end // end of [list_append2]
diff --git a/test/data/list_append.out b/test/data/list_append.out
new file mode 100644
--- /dev/null
+++ b/test/data/list_append.out
@@ -0,0 +1,39 @@
+fun {a:t@ype} list_append { m, n : nat }( xs : list(a, m)
+                                        , ys : list(a, n)
+                                        ) : list(a, m+n) =
+  (case+ xs of
+    | list_cons (x, xs) => list_cons((x, list_append(xs, ys)))
+    | list_nil () => ys)
+
+// end of [list_append]
+fun {a:t@ype} list_append2 { m, n : nat }( xs : list(a, m)
+                                         , ys : list(a, n)
+                                         ) : list(a, m+n) =
+  let
+    //
+    fun loop {m:nat}( xs : list(a, m)
+                    , ys : list(a, n)
+                    , res : &ptr? >> list(a, m+n)
+                    ) : void =
+      (case+ xs of
+        | list_cons (x, xs1) => let
+          val () = res := list_cons{a}{0}(x, _)
+          val+ list_cons (_, res1) = res
+          val () = loop((xs1, ys, res1))
+          
+          // of [xs1] and [ys]
+        in
+          fold@(res)
+        end
+        | list_nil () => res := ys)
+    
+    //
+    var res: ptr
+    val () = loop((xs, ys, res))
+    
+    //
+  in
+    res
+  end
+
+// end of [list_append2]
diff --git a/test/data/prf_sqrt2.dats b/test/data/prf_sqrt2.dats
new file mode 100644
--- /dev/null
+++ b/test/data/prf_sqrt2.dats
@@ -0,0 +1,130 @@
+(*
+** Some code used in the book INT2PROGINATS
+*)
+
+(* ****** ****** *)
+
+abstype
+MOD0(m: int, p: int) // m=p*q
+  
+(* ****** ****** *)
+//
+extern
+prfun
+lemma_MOD0_intr
+  {m,p,q:nat | m==p*q}(): MOD0(m, p)
+extern
+prfun
+lemma_MOD0_elim
+  {m,p:int}
+  (MOD0(m, p)): [q:nat] EQINT(m, p*q)
+//
+(* ****** ****** *)
+
+abstype PRIME(p:int)
+
+(* ****** ****** *)
+//
+extern
+prfun
+lemma_PRIME_param
+  {p:int}(pf: PRIME(p)): [p >= 2] void
+//
+(* ****** ****** *)
+//
+extern
+prfun
+mylemma1{n,p:int}
+  (MOD0(n*n, p), PRIME(p)): MOD0(n, p)
+//
+(* ****** ****** *)
+
+extern
+prfun
+mylemma_main
+{m,n,p:int | m*m==p*n*n}(PRIME(p)): [m2:nat | n*n==p*m2*m2] void
+
+(* ****** ****** *)
+
+extern
+prfun
+square_is_nat{m:int}(): [m*m>=0] void
+
+(* ****** ****** *)
+
+primplmnt
+mylemma_main
+{m,n,p}(pfprm) = let
+  prval pfeq_mm_pnn =
+    eqint_make{m*m,p*n*n}()
+  prval () = square_is_nat{m}()
+  prval () = square_is_nat{n}()
+  prval () = lemma_PRIME_param(pfprm)
+  prval
+  pfmod1 =
+    lemma_MOD0_intr{m*m,p,n*n}()
+  prval
+  pfmod2 = mylemma1{m,p}(pfmod1, pfprm)
+  prval
+  [m2:int]
+  EQINT() =
+    lemma_MOD0_elim(pfmod2)
+  prval EQINT() = pfeq_mm_pnn
+  prval () =
+  __assert{p}{p*m2*m2,n*n}() where
+  {
+    extern prfun __assert{p:pos}{x,y:int | p*x==p*y}(): [x==y] void
+  }
+in
+  0
+end // end of [mylemma_main]
+
+(* ****** ****** *)
+//
+extern
+prfun
+sqrt2_irrat
+{m,n:nat |
+ n >= 1; m*m==2*n*n}((*void*)): [false] void
+//
+(* ****** ****** *)
+
+primplmnt
+sqrt2_irrat
+  {m,n}((*void*)) = let
+prfun
+auxmain 
+{m,n:nat |
+ n >= 1;
+ m*m==2*n*n} .<m>.
+(
+// argless
+) : [false] void = let
+//
+prval pfprm =
+__assert() where
+{
+  extern praxi __assert(): PRIME(2)
+}
+prval
+[m2:int] () = mylemma_main{m,n,2}(pfprm)
+//
+prval () =
+__assert() where { extern praxi __assert(): [m > n] void }
+prval () =
+__assert() where { extern praxi __assert(): [m2 >= 1] void }
+//
+in
+  auxmain{n,m2}()
+end
+in
+  auxmain{m,n}()
+end // end of [sqrt2_irrat]
+
+(* ****** ****** *)
+
+implement main0 () = ()
+
+(* ****** ****** *)
+
+(* end of [sqrt2_irrat.dats] *)
diff --git a/test/data/prf_sqrt2.out b/test/data/prf_sqrt2.out
new file mode 100644
--- /dev/null
+++ b/test/data/prf_sqrt2.out
@@ -0,0 +1,101 @@
+(*
+** Some code used in the book INT2PROGINATS
+*)
+(* ****** ****** *)
+abstype MOD0(m: int, p: int)
+
+// m=p*q
+(* ****** ****** *)
+//
+extern
+prfun lemma_MOD0_intr { m, p, q : nat | m == p*q } () : MOD0(m, p)
+
+extern
+prfun lemma_MOD0_elim { m, p : int } (MOD0(m,p)) : [q:nat] EQINT(m, p*q)
+
+//
+(* ****** ****** *)
+abstype PRIME(p: int)
+
+(* ****** ****** *)
+//
+extern
+prfun lemma_PRIME_param {p:int} (pf : PRIME(p)) : [p >= 2] void
+
+//
+(* ****** ****** *)
+//
+extern
+prfun mylemma1 { n, p : int } (MOD0(n*n,p), PRIME(p)) : MOD0(n, p)
+
+//
+(* ****** ****** *)
+extern
+prfun mylemma_main { m, n, p : int | m*m == p*n*n } (PRIME(p)) :
+  [ m2 : nat | n*n == p*m2*m2 ] void
+
+(* ****** ****** *)
+extern
+prfun square_is_nat {m:int} () : [m*m >= 0] void
+
+(* ****** ****** *)
+primplmnt mylemma_main {m,n,p} (pfprm) =
+  let
+    prval pfeq_mm_pnn = eqint_make{m*m,p*n*n}()
+    prval () = square_is_nat{m}()
+    prval () = square_is_nat{n}()
+    prval () = lemma_PRIME_param(pfprm)
+    prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}()
+    prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm)
+    prval [m2:int]EQINT() = lemma_MOD0_elim(pfmod2)
+    prval EQINT() = pfeq_mm_pnn
+    prval () = __assert{p}{p*m2*m2,n*n}() where
+    { extern
+      prfun __assert {p:pos}{ x, y : int | p*x == p*y } () : [x == y] void }
+  in
+    0
+  end
+
+// end of [mylemma_main]
+(* ****** ****** *)
+//
+extern
+prfun sqrt2_irrat { m, n : nat | n >= 1; m*m == 2*n*n } () :
+  [false] void
+
+//
+(* ****** ****** *)
+primplmnt sqrt2_irrat {m,n} () =
+  let
+    prfun auxmain { m, n : nat | n >= 1; m*m == 2*n*n } .<m>. () :
+      [false] void =
+      let
+        //
+        prval pfprm = __assert() where
+        { extern
+          praxi __assert() : PRIME(2) }
+        prval [m2:int]() = mylemma_main{m,n,2}(pfprm)
+        
+        //
+        prval () = __assert() where
+        { extern
+          praxi __assert() : [m > n] void }
+        prval () = __assert() where
+        { extern
+          praxi __assert() : [m2 >= 1] void }
+        
+        //
+      in
+        auxmain{n,m2}()
+      end
+  in
+    auxmain{m,n}()
+  end
+
+// end of [sqrt2_irrat]
+(* ****** ****** *)
+implement main0 () =
+  ()
+
+(* ****** ****** *)
+(* end of [sqrt2_irrat.dats] *)
diff --git a/test/data/stdlib/array.out b/test/data/stdlib/array.out
--- a/test/data/stdlib/array.out
+++ b/test/data/stdlib/array.out
@@ -321,7 +321,6 @@
 //
 fun {a:vt0p} array_tabulate$fopr (i : size_t) : (a)
 
-//
 fun {a:vt0p} array_ptr_tabulate {n:int} (asz : size_t(n)) :
   [l:addr] (array_v(a, l, n), mfree_gc_v(l)| ptr(l))
 
diff --git a/test/data/stdlib/arrayref.out b/test/data/stdlib/arrayref.out
--- a/test/data/stdlib/arrayref.out
+++ b/test/data/stdlib/arrayref.out
@@ -140,7 +140,6 @@
 //
 fun {a:t0p} arrayref_head {n:pos} (A : arrayref(a, n)) :<!ref> (a)
 
-// A[0]
 fun {a:t0p} arrayref_tail {n:pos} (A : arrayref(a, n)) :<!ref>
   arrayref(a, n-1)
 
@@ -150,12 +149,10 @@
 fun {a:t0p}{tk:tk} arrayref_get_at_gint {n:int}{ i : nat | i < n }
 (A0 : arrayref(a, n), i : g1int(tk, i)) :<!ref> (a)
 
-// arrayref_get_at_gint
 //
 fun {a:t0p}{tk:tk} arrayref_get_at_guint {n:int}{ i : nat | i < n }
 (A0 : arrayref(a, n), i : g1uint(tk, i)) :<!ref> (a)
 
-// arrayref_get_at_guint
 //
 symintr arrayref_get_at
 
diff --git a/test/data/stdlib/basics_dyn.out b/test/data/stdlib/basics_dyn.out
--- a/test/data/stdlib/basics_dyn.out
+++ b/test/data/stdlib/basics_dyn.out
@@ -218,10 +218,8 @@
 //
 fun {a:t0p} lazy_force (lazyval : lazy(INV(a))) :<!laz> (a)
 
-//
 fun {a:vt0p} lazy_vt_force (lazyval : lazy_vt(INV(a))) :<!all> (a)
 
-//
 (*
 //
 // HX-2016-08:
@@ -436,7 +434,6 @@
 
 fun {a:vtype} unbox_vt  : boxed_vt(INV(a)) -> (a)
 
-//
 (* ****** ****** *)
 //
 stadef array (a: vt@ype, n: int) = @[a][n]
@@ -562,7 +559,6 @@
 //
 fun {a:vt0p} opt_unsome_get (x : &opt(INV(a), true) >> a?) : (a)
 
-//
 praxi opt_none {a:vt0p} (x : !(a?) >> opt(a, false)) :<prf> void
 
 praxi opt_unnone {a:vt0p} (x : !opt(INV(a), false) >> a?) :<prf> void
@@ -581,7 +577,6 @@
   | VOR_l(a0, a1, 0) of (INV(a0))
   | VOR_r(a0, a1, 1) of (INV(a1))
 
-//
 stadef por  = or_prop_prop_int_prop
 stadef vor  = or_view_view_int_view
 
diff --git a/test/data/stdlib/gorder.out b/test/data/stdlib/gorder.out
--- a/test/data/stdlib/gorder.out
+++ b/test/data/stdlib/gorder.out
@@ -110,7 +110,6 @@
 
 fun {a:t0p} gmin_val_val (x : a, y : a) :<> (a)
 
-//
 (* ****** ****** *)
 //
 fun {a:vt0p} glt_ref_ref (x : &INV(a), y : &a) :<> bool
diff --git a/test/data/stdlib/option_vt.out b/test/data/stdlib/option_vt.out
--- a/test/data/stdlib/option_vt.out
+++ b/test/data/stdlib/option_vt.out
@@ -71,7 +71,6 @@
 fun {a:vt0p} option_vt_unsome (opt : option_vt(INV(a), true)) :<!wrt>
   (a)
 
-//
 fun {a:vt0p} option_vt_unnone (opt : option_vt(INV(a), false)) :<!wrt>
   void
 
diff --git a/test/data/stdlib/unsafe.out b/test/data/stdlib/unsafe.out
--- a/test/data/stdlib/unsafe.out
+++ b/test/data/stdlib/unsafe.out
@@ -199,7 +199,6 @@
 
 fun {a:vt0p} ptr1_get (p : Ptr1) :<> (a)
 
-//
 fun {a:vt0p} ptr0_set (p : ptr, x : INV(a)) :<!wrt> void
 
 fun {a:vt0p} ptr1_set (p : Ptr1, x : INV(a)) :<!wrt> void
@@ -222,7 +221,6 @@
 fun {a:vt0p} ptr1_getinc {l:addr} (p : &ptr(l) >> ptr(l+sizeof(a))) :
   (a)
 
-//
 fun {a:vt0p} ptr0_setinc (p : &ptr >> _, x : a) : void
 
 fun {a:vt0p} ptr1_setinc {l:addr} ( p : &ptr(l) >> ptr(l+sizeof(a))