diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,13 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.5.4 — 2022-08-19
+
+This version contains minor improvements:
+
+1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));
+2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).
+
 ## v0.5.3 — 2022-07-12
 
 This version contains a few minor improvements:
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.2.
+-- This file has been generated from package.yaml by hpack version 0.35.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.5.3
+version:        0.5.4
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
diff --git a/src/Language/Rzk/Syntax/Lex.x b/src/Language/Rzk/Syntax/Lex.x
new file mode 100644
--- /dev/null
+++ b/src/Language/Rzk/Syntax/Lex.x
@@ -0,0 +1,292 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).
+
+-- Lexer definition for use with Alex 3
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+
+module Language.Rzk.Syntax.Lex where
+
+import Prelude
+
+import qualified Data.Bits
+import Data.Char     (ord)
+import Data.Function (on)
+import Data.Word     (Word8)
+}
+
+-- Predefined character classes
+
+$c = [A-Z\192-\221] # [\215]  -- capital isolatin1 letter (215 = \times) FIXME
+$s = [a-z\222-\255] # [\247]  -- small   isolatin1 letter (247 = \div  ) FIXME
+$l = [$c $s]         -- letter
+$d = [0-9]           -- digit
+$i = [$l $d _ ']     -- identifier character
+$u = [. \n]          -- universal: any character
+
+-- Symbols and non-identifier-like reserved words
+
+@rsyms = \Σ | \π \₁ | \π \₂ | \# "lang" | \; | "rzk" \- "1" | \# "set" \- "option" | \= | \# "unset" \- "option" | \# "check" | \: | \# "compute" | \# "compute" \- "whnf" | \# "compute" \- "nf" | \# "postulate" | \# "assume" | \# "variable" | \# "variables" | \# "section" | \# "end" | \# "define" | \: \= | \# "def" | \( | \) | \, | \| | \{ | \} | \↦ | "1" | \* \₁ | "2" | "0" \₂ | "1" \₂ | \× | \⊤ | \⊥ | \≡ | \≤ | \∧ | \∨ | \→ | \= \_ \{ | \[ | \] | \< | \> | \\ | "refl" \_ \{ | \* | \* \_ "1" | "0" \_ "2" | "1" \_ "2" | \= \= \= | \< \= | \/ \\ | \\ \/ | \- \> | \| \- \> | \∑
+
+:-
+
+-- Line comment "--"
+"--" [.]* ;
+
+-- Block comment "{-" "-}"
+\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;
+
+-- Whitespace (skipped)
+$white+ ;
+
+-- Symbols
+@rsyms
+    { tok (eitherResIdent TV) }
+
+-- token VarIdentToken
+[$u # [\t \n \r \  \! \" \# \( \) \, \- \. \; \< \> \? \[ \\ \] \{ \| \}]] [$u # [\t \n \r \  \" \# \( \) \, \; \< \> \[ \\ \] \{ \| \}]] *
+    { tok (eitherResIdent T_VarIdentToken) }
+
+-- token HoleIdentToken
+\?
+    { tok (eitherResIdent T_HoleIdentToken) }
+
+-- Keywords and Ident
+$l $i*
+    { tok (eitherResIdent TV) }
+
+-- String
+\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \"
+    { tok (TL . unescapeInitTail) }
+
+{
+-- | Create a token with position.
+tok :: (String -> Tok) -> (Posn -> String -> Token)
+tok f p = PT p . f
+
+-- | Token without position.
+data Tok
+  = TK {-# UNPACK #-} !TokSymbol  -- ^ Reserved word or symbol.
+  | TL !String                    -- ^ String literal.
+  | TI !String                    -- ^ Integer literal.
+  | TV !String                    -- ^ Identifier.
+  | TD !String                    -- ^ Float literal.
+  | TC !String                    -- ^ Character literal.
+  | T_VarIdentToken !String
+  | T_HoleIdentToken !String
+  deriving (Eq, Show, Ord)
+
+-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
+pattern TS :: String -> Int -> Tok
+pattern TS t i = TK (TokSymbol t i)
+
+-- | Keyword or symbol tokens have a unique ID.
+data TokSymbol = TokSymbol
+  { tsText :: String
+      -- ^ Keyword or symbol text.
+  , tsID   :: !Int
+      -- ^ Unique ID.
+  } deriving (Show)
+
+-- | Keyword/symbol equality is determined by the unique ID.
+instance Eq  TokSymbol where (==)    = (==)    `on` tsID
+
+-- | Keyword/symbol ordering is determined by the unique ID.
+instance Ord TokSymbol where compare = compare `on` tsID
+
+-- | Token with position.
+data Token
+  = PT  Posn Tok
+  | Err Posn
+  deriving (Eq, Show, Ord)
+
+-- | Pretty print a position.
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+-- | Pretty print the position of the first token in the list.
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos []    = "end of file"
+
+-- | Get the position of a token.
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p)  = p
+
+-- | Get line and column of a token.
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+-- | Get line and column of a position.
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+-- | Convert a token into "position token" form.
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t = (tokenLineCol t, tokenText t)
+
+-- | Convert a token to its text.
+tokenText :: Token -> String
+tokenText t = case t of
+  PT _ (TS s _) -> s
+  PT _ (TL s)   -> show s
+  PT _ (TI s)   -> s
+  PT _ (TV s)   -> s
+  PT _ (TD s)   -> s
+  PT _ (TC s)   -> s
+  Err _         -> "#error"
+  PT _ (T_VarIdentToken s) -> s
+  PT _ (T_HoleIdentToken s) -> s
+
+-- | Convert a token to a string.
+prToken :: Token -> String
+prToken t = tokenText t
+
+-- | Finite map from text to token organized as binary search tree.
+data BTree
+  = N -- ^ Nil (leaf).
+  | B String Tok BTree BTree
+      -- ^ Binary node.
+  deriving (Show)
+
+-- | Convert potential keyword into token or use fallback conversion.
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+  where
+  treeFind N = tv s
+  treeFind (B a t left right) =
+    case compare s a of
+      LT -> treeFind left
+      GT -> treeFind right
+      EQ -> t
+
+-- | The keywords and symbols of the language organized as binary search tree.
+resWords :: BTree
+resWords =
+  b "BOT" 39
+    (b "*\8321" 20
+       (b "#postulate" 10
+          (b "#compute-whnf" 5
+             (b "#compute" 3
+                (b "#check" 2 (b "#assume" 1 N N) N) (b "#compute-nf" 4 N N))
+             (b "#end" 8 (b "#define" 7 (b "#def" 6 N N) N) (b "#lang" 9 N N)))
+          (b "#variables" 15
+             (b "#unset-option" 13
+                (b "#set-option" 12 (b "#section" 11 N N) N)
+                (b "#variable" 14 N N))
+             (b "*" 18 (b ")" 17 (b "(" 16 N N) N) (b "*_1" 19 N N))))
+       (b ":" 30
+          (b "0\8322" 25
+             (b "/\\" 23 (b "->" 22 (b "," 21 N N) N) (b "0_2" 24 N N))
+             (b "1\8322" 28 (b "1_2" 27 (b "1" 26 N N) N) (b "2" 29 N N)))
+          (b "=" 35
+             (b "<" 33 (b ";" 32 (b ":=" 31 N N) N) (b "<=" 34 N N))
+             (b "=_{" 37 (b "===" 36 N N) (b ">" 38 N N)))))
+    (b "unit" 59
+       (b "]" 49
+          (b "U" 44
+             (b "TOP" 42 (b "Sigma" 41 (b "CUBE" 40 N N) N) (b "TOPE" 43 N N))
+             (b "\\" 47 (b "[" 46 (b "Unit" 45 N N) N) (b "\\/" 48 N N)))
+          (b "recOR" 54
+             (b "idJ" 52 (b "first" 51 (b "as" 50 N N) N) (b "recBOT" 53 N N))
+             (b "rzk-1" 57
+                (b "refl_{" 56 (b "refl" 55 N N) N) (b "second" 58 N N))))
+       (b "\8594" 69
+          (b "}" 64
+             (b "|" 62 (b "{" 61 (b "uses" 60 N N) N) (b "|->" 63 N N))
+             (b "\960\8321" 67
+                (b "\931" 66 (b "\215" 65 N N) N) (b "\960\8322" 68 N N)))
+          (b "\8801" 74
+             (b "\8743" 72
+                (b "\8721" 71 (b "\8614" 70 N N) N) (b "\8744" 73 N N))
+             (b "\8868" 76 (b "\8804" 75 N N) (b "\8869" 77 N N)))))
+  where
+  b s n = B bs (TS bs n)
+    where
+    bs = s
+
+-- | Unquote string literal.
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id
+  where
+  unesc s = case s of
+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+    '\\':'n':cs  -> '\n' : unesc cs
+    '\\':'t':cs  -> '\t' : unesc cs
+    '\\':'r':cs  -> '\r' : unesc cs
+    '\\':'f':cs  -> '\f' : unesc cs
+    '"':[]       -> []
+    c:cs         -> c : unesc cs
+    _            -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+  deriving (Eq, Show, Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1
+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn,     -- current position,
+                  Char,     -- previous char
+                  [Byte],   -- pending bytes on the current char
+                  String)   -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+    where
+      go :: AlexInput -> [Token]
+      go inp@(pos, _, _, str) =
+               case alexScan inp 0 of
+                AlexEOF                   -> []
+                AlexError (pos, _, _, _)  -> [Err pos]
+                AlexSkip  inp' len        -> go inp'
+                AlexToken inp' len act    -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+  case s of
+    []  -> Nothing
+    (c:s) ->
+             let p'     = alexMove p c
+                 (b:bs) = utf8Encode c
+              in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+  where
+  go oc
+   | oc <= 0x7f       = [oc]
+
+   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+
+   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+}
diff --git a/src/Language/Rzk/Syntax/Par.y b/src/Language/Rzk/Syntax/Par.y
new file mode 100644
--- /dev/null
+++ b/src/Language/Rzk/Syntax/Par.y
@@ -0,0 +1,456 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).
+
+-- Parser definition for use with Happy
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Language.Rzk.Syntax.Par
+  ( happyError
+  , myLexer
+  , pModule
+  , pHoleIdent
+  , pVarIdent
+  , pListVarIdent
+  , pLanguageDecl
+  , pLanguage
+  , pCommand
+  , pListCommand
+  , pDeclUsedVars
+  , pSectionName
+  , pPattern
+  , pListPattern
+  , pParam
+  , pListParam
+  , pParamDecl
+  , pRestriction
+  , pListRestriction
+  , pTerm7
+  , pTerm5
+  , pTerm4
+  , pTerm3
+  , pTerm2
+  , pTerm1
+  , pTerm6
+  , pTerm
+  , pListTerm
+  ) where
+
+import Prelude
+
+import qualified Language.Rzk.Syntax.Abs
+import Language.Rzk.Syntax.Lex
+
+}
+
+%name pModule_internal Module
+%name pHoleIdent_internal HoleIdent
+%name pVarIdent_internal VarIdent
+%name pListVarIdent_internal ListVarIdent
+%name pLanguageDecl_internal LanguageDecl
+%name pLanguage_internal Language
+%name pCommand_internal Command
+%name pListCommand_internal ListCommand
+%name pDeclUsedVars_internal DeclUsedVars
+%name pSectionName_internal SectionName
+%name pPattern_internal Pattern
+%name pListPattern_internal ListPattern
+%name pParam_internal Param
+%name pListParam_internal ListParam
+%name pParamDecl_internal ParamDecl
+%name pRestriction_internal Restriction
+%name pListRestriction_internal ListRestriction
+%name pTerm7_internal Term7
+%name pTerm5_internal Term5
+%name pTerm4_internal Term4
+%name pTerm3_internal Term3
+%name pTerm2_internal Term2
+%name pTerm1_internal Term1
+%name pTerm6_internal Term6
+%name pTerm_internal Term
+%name pListTerm_internal ListTerm
+-- no lexer declaration
+%monad { Err } { (>>=) } { return }
+%tokentype {Token}
+%token
+  '#assume'        { PT _ (TS _ 1)             }
+  '#check'         { PT _ (TS _ 2)             }
+  '#compute'       { PT _ (TS _ 3)             }
+  '#compute-nf'    { PT _ (TS _ 4)             }
+  '#compute-whnf'  { PT _ (TS _ 5)             }
+  '#def'           { PT _ (TS _ 6)             }
+  '#define'        { PT _ (TS _ 7)             }
+  '#end'           { PT _ (TS _ 8)             }
+  '#lang'          { PT _ (TS _ 9)             }
+  '#postulate'     { PT _ (TS _ 10)            }
+  '#section'       { PT _ (TS _ 11)            }
+  '#set-option'    { PT _ (TS _ 12)            }
+  '#unset-option'  { PT _ (TS _ 13)            }
+  '#variable'      { PT _ (TS _ 14)            }
+  '#variables'     { PT _ (TS _ 15)            }
+  '('              { PT _ (TS _ 16)            }
+  ')'              { PT _ (TS _ 17)            }
+  '*'              { PT _ (TS _ 18)            }
+  '*_1'            { PT _ (TS _ 19)            }
+  '*₁'             { PT _ (TS _ 20)            }
+  ','              { PT _ (TS _ 21)            }
+  '->'             { PT _ (TS _ 22)            }
+  '/\\'            { PT _ (TS _ 23)            }
+  '0_2'            { PT _ (TS _ 24)            }
+  '0₂'             { PT _ (TS _ 25)            }
+  '1'              { PT _ (TS _ 26)            }
+  '1_2'            { PT _ (TS _ 27)            }
+  '1₂'             { PT _ (TS _ 28)            }
+  '2'              { PT _ (TS _ 29)            }
+  ':'              { PT _ (TS _ 30)            }
+  ':='             { PT _ (TS _ 31)            }
+  ';'              { PT _ (TS _ 32)            }
+  '<'              { PT _ (TS _ 33)            }
+  '<='             { PT _ (TS _ 34)            }
+  '='              { PT _ (TS _ 35)            }
+  '==='            { PT _ (TS _ 36)            }
+  '=_{'            { PT _ (TS _ 37)            }
+  '>'              { PT _ (TS _ 38)            }
+  'BOT'            { PT _ (TS _ 39)            }
+  'CUBE'           { PT _ (TS _ 40)            }
+  'Sigma'          { PT _ (TS _ 41)            }
+  'TOP'            { PT _ (TS _ 42)            }
+  'TOPE'           { PT _ (TS _ 43)            }
+  'U'              { PT _ (TS _ 44)            }
+  'Unit'           { PT _ (TS _ 45)            }
+  '['              { PT _ (TS _ 46)            }
+  '\\'             { PT _ (TS _ 47)            }
+  '\\/'            { PT _ (TS _ 48)            }
+  ']'              { PT _ (TS _ 49)            }
+  'as'             { PT _ (TS _ 50)            }
+  'first'          { PT _ (TS _ 51)            }
+  'idJ'            { PT _ (TS _ 52)            }
+  'recBOT'         { PT _ (TS _ 53)            }
+  'recOR'          { PT _ (TS _ 54)            }
+  'refl'           { PT _ (TS _ 55)            }
+  'refl_{'         { PT _ (TS _ 56)            }
+  'rzk-1'          { PT _ (TS _ 57)            }
+  'second'         { PT _ (TS _ 58)            }
+  'unit'           { PT _ (TS _ 59)            }
+  'uses'           { PT _ (TS _ 60)            }
+  '{'              { PT _ (TS _ 61)            }
+  '|'              { PT _ (TS _ 62)            }
+  '|->'            { PT _ (TS _ 63)            }
+  '}'              { PT _ (TS _ 64)            }
+  '×'              { PT _ (TS _ 65)            }
+  'Σ'              { PT _ (TS _ 66)            }
+  'π₁'             { PT _ (TS _ 67)            }
+  'π₂'             { PT _ (TS _ 68)            }
+  '→'              { PT _ (TS _ 69)            }
+  '↦'              { PT _ (TS _ 70)            }
+  '∑'              { PT _ (TS _ 71)            }
+  '∧'              { PT _ (TS _ 72)            }
+  '∨'              { PT _ (TS _ 73)            }
+  '≡'              { PT _ (TS _ 74)            }
+  '≤'              { PT _ (TS _ 75)            }
+  '⊤'              { PT _ (TS _ 76)            }
+  '⊥'              { PT _ (TS _ 77)            }
+  L_quoted         { PT _ (TL _)               }
+  L_VarIdentToken  { PT _ (T_VarIdentToken _)  }
+  L_HoleIdentToken { PT _ (T_HoleIdentToken _) }
+
+%%
+
+String  :: { (Language.Rzk.Syntax.Abs.BNFC'Position, String) }
+String   : L_quoted { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), ((\(PT _ (TL s)) -> s) $1)) }
+
+VarIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdentToken) }
+VarIdentToken  : L_VarIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.VarIdentToken (tokenText $1)) }
+
+HoleIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdentToken) }
+HoleIdentToken  : L_HoleIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.HoleIdentToken (tokenText $1)) }
+
+Module :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Module) }
+Module
+  : LanguageDecl ListCommand { (fst $1, Language.Rzk.Syntax.Abs.Module (fst $1) (snd $1) (snd $2)) }
+
+HoleIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdent) }
+HoleIdent
+  : HoleIdentToken { (fst $1, Language.Rzk.Syntax.Abs.HoleIdent (fst $1) (snd $1)) }
+
+VarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdent) }
+VarIdent
+  : VarIdentToken { (fst $1, Language.Rzk.Syntax.Abs.VarIdent (fst $1) (snd $1)) }
+
+ListVarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.VarIdent]) }
+ListVarIdent
+  : VarIdent { (fst $1, (:[]) (snd $1)) }
+  | VarIdent ListVarIdent { (fst $1, (:) (snd $1) (snd $2)) }
+
+LanguageDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.LanguageDecl) }
+LanguageDecl
+  : '#lang' Language ';' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.LanguageDecl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+
+Language :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Language) }
+Language
+  : 'rzk-1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Rzk1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+
+Command :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Command) }
+Command
+  : '#set-option' String '=' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#unset-option' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandUnsetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#check' Term ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCheck (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#compute' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCompute (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#compute-whnf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeWHNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#compute-nf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#postulate' VarIdent DeclUsedVars ListParam ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandPostulate (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6)) }
+  | '#postulate' VarIdent DeclUsedVars ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandPostulateNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5)) }
+  | '#assume' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandAssume (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#variable' VarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariable (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#variables' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariables (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#section' SectionName ';' ListCommand '#end' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSection (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+  | '#define' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandDefine (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }
+  | '#define' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefineNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }
+  | '#def' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDef (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }
+  | '#def' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }
+
+ListCommand :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Command]) }
+ListCommand
+  : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, []) }
+  | Command ';' ListCommand { (fst $1, (:) (snd $1) (snd $3)) }
+
+DeclUsedVars :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.DeclUsedVars) }
+DeclUsedVars
+  : 'uses' '(' ListVarIdent ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.DeclUsedVars (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }
+  | {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.noDeclUsedVars Language.Rzk.Syntax.Abs.BNFC'NoPosition) }
+
+SectionName :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SectionName) }
+SectionName
+  : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.NoSectionName Language.Rzk.Syntax.Abs.BNFC'NoPosition) }
+  | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.SomeSectionName (fst $1) (snd $1)) }
+
+Pattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Pattern) }
+Pattern
+  : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) }
+  | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+
+ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }
+ListPattern
+  : Pattern { (fst $1, (:[]) (snd $1)) }
+  | Pattern ListPattern { (fst $1, (:) (snd $1) (snd $2)) }
+
+Param :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Param) }
+Param
+  : Pattern { (fst $1, Language.Rzk.Syntax.Abs.ParamPattern (fst $1) (snd $1)) }
+  | '(' ListPattern ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' ListPattern ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+  | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+
+ListParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Param]) }
+ListParam
+  : Param { (fst $1, (:[]) (snd $1)) }
+  | Param ListParam { (fst $1, (:) (snd $1) (snd $2)) }
+
+ParamDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.ParamDecl) }
+ParamDecl
+  : Term6 { (fst $1, Language.Rzk.Syntax.Abs.ParamType (fst $1) (snd $1)) }
+  | '(' Term ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Term ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+  | '{' Pattern ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '{' '(' Pattern ':' Term ')' '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.paramVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+
+Restriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Restriction) }
+Restriction
+  : Term '↦' Term { (fst $1, Language.Rzk.Syntax.Abs.Restriction (fst $1) (snd $1) (snd $3)) }
+  | Term '|->' Term { (fst $1, Language.Rzk.Syntax.Abs.ASCII_Restriction (fst $1) (snd $1) (snd $3)) }
+
+ListRestriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Restriction]) }
+ListRestriction
+  : Restriction { (fst $1, (:[]) (snd $1)) }
+  | Restriction ',' ListRestriction { (fst $1, (:) (snd $1) (snd $3)) }
+
+Term7 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term7
+  : 'U' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Universe (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'CUBE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseCube (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'TOPE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseTope (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '*₁' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '0₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '1₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '⊤' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '⊥' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'recBOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'recOR' '(' ListRestriction ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOr (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }
+  | 'recOR' '(' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOrDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9)) }
+  | 'Unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '<' ParamDecl '→' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Pair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Unit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'refl' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Refl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'refl_{' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTerm (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | 'refl_{' Term ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | 'idJ' '(' Term ',' Term ',' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.IdJ (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9) (snd $11) (snd $13)) }
+  | HoleIdent { (fst $1, Language.Rzk.Syntax.Abs.Hole (fst $1) (snd $1)) }
+  | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.Var (fst $1) (snd $1)) }
+  | '(' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), (snd $2)) }
+  | '*_1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '0_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '1_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'TOP' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'BOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '<' ParamDecl '->' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+
+Term5 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term5
+  : Term5 '×' Term6 { (fst $1, Language.Rzk.Syntax.Abs.CubeProduct (fst $1) (snd $1) (snd $3)) }
+  | Term6 { (fst $1, (snd $1)) }
+  | Term5 '*' Term6 { (fst $1, Language.Rzk.Syntax.Abs.ascii_CubeProduct (fst $1) (snd $1) (snd $3)) }
+
+Term4 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term4
+  : Term5 '≡' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeEQ (fst $1) (snd $1) (snd $3)) }
+  | Term5 '≤' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeLEQ (fst $1) (snd $1) (snd $3)) }
+  | Term5 { (fst $1, (snd $1)) }
+  | Term5 '===' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeEQ (fst $1) (snd $1) (snd $3)) }
+  | Term5 '<=' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeLEQ (fst $1) (snd $1) (snd $3)) }
+
+Term3 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term3
+  : Term4 '∧' Term3 { (fst $1, Language.Rzk.Syntax.Abs.TopeAnd (fst $1) (snd $1) (snd $3)) }
+  | Term4 { (fst $1, (snd $1)) }
+  | Term4 '/\\' Term3 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeAnd (fst $1) (snd $1) (snd $3)) }
+
+Term2 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term2
+  : Term3 '∨' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TopeOr (fst $1) (snd $1) (snd $3)) }
+  | Term3 { (fst $1, (snd $1)) }
+  | Term3 '\\/' Term2 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeOr (fst $1) (snd $1) (snd $3)) }
+
+Term1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term1
+  : ParamDecl '→' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) }
+  | 'Σ' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | Term2 '=_{' Term '}' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeId (fst $1) (snd $1) (snd $3) (snd $5)) }
+  | Term2 '=' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeIdSimple (fst $1) (snd $1) (snd $3)) }
+  | '\\' ListParam '→' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | Term2 { (fst $1, (snd $1)) }
+  | ParamDecl '->' Term1 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TypeFun (fst $1) (snd $1) (snd $3)) }
+  | 'Sigma' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | '\\' ListParam '->' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '∑' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+
+Term6 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term6
+  : Term6 '[' ListRestriction ']' { (fst $1, Language.Rzk.Syntax.Abs.TypeRestricted (fst $1) (snd $1) (snd $3)) }
+  | Term6 Term7 { (fst $1, Language.Rzk.Syntax.Abs.App (fst $1) (snd $1) (snd $2)) }
+  | 'π₁' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | 'π₂' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | Term7 { (fst $1, (snd $1)) }
+  | 'first' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | 'second' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+
+Term :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term
+  : Term2 'as' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeAsc (fst $1) (snd $1) (snd $3)) }
+  | Term1 { (fst $1, (snd $1)) }
+
+ListTerm :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Term]) }
+ListTerm
+  : Term { (fst $1, (:[]) (snd $1)) }
+  | Term ',' ListTerm { (fst $1, (:) (snd $1) (snd $3)) }
+
+{
+
+type Err = Either String
+
+happyError :: [Token] -> Err a
+happyError ts = Left $
+  "syntax error at " ++ tokenPos ts ++
+  case ts of
+    []      -> []
+    [Err _] -> " due to lexer error"
+    t:_     -> " before `" ++ (prToken t) ++ "'"
+
+myLexer :: String -> [Token]
+myLexer = tokens
+
+-- Entrypoints
+
+pModule :: [Token] -> Err Language.Rzk.Syntax.Abs.Module
+pModule = fmap snd . pModule_internal
+
+pHoleIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.HoleIdent
+pHoleIdent = fmap snd . pHoleIdent_internal
+
+pVarIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.VarIdent
+pVarIdent = fmap snd . pVarIdent_internal
+
+pListVarIdent :: [Token] -> Err [Language.Rzk.Syntax.Abs.VarIdent]
+pListVarIdent = fmap snd . pListVarIdent_internal
+
+pLanguageDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.LanguageDecl
+pLanguageDecl = fmap snd . pLanguageDecl_internal
+
+pLanguage :: [Token] -> Err Language.Rzk.Syntax.Abs.Language
+pLanguage = fmap snd . pLanguage_internal
+
+pCommand :: [Token] -> Err Language.Rzk.Syntax.Abs.Command
+pCommand = fmap snd . pCommand_internal
+
+pListCommand :: [Token] -> Err [Language.Rzk.Syntax.Abs.Command]
+pListCommand = fmap snd . pListCommand_internal
+
+pDeclUsedVars :: [Token] -> Err Language.Rzk.Syntax.Abs.DeclUsedVars
+pDeclUsedVars = fmap snd . pDeclUsedVars_internal
+
+pSectionName :: [Token] -> Err Language.Rzk.Syntax.Abs.SectionName
+pSectionName = fmap snd . pSectionName_internal
+
+pPattern :: [Token] -> Err Language.Rzk.Syntax.Abs.Pattern
+pPattern = fmap snd . pPattern_internal
+
+pListPattern :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]
+pListPattern = fmap snd . pListPattern_internal
+
+pParam :: [Token] -> Err Language.Rzk.Syntax.Abs.Param
+pParam = fmap snd . pParam_internal
+
+pListParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.Param]
+pListParam = fmap snd . pListParam_internal
+
+pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl
+pParamDecl = fmap snd . pParamDecl_internal
+
+pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction
+pRestriction = fmap snd . pRestriction_internal
+
+pListRestriction :: [Token] -> Err [Language.Rzk.Syntax.Abs.Restriction]
+pListRestriction = fmap snd . pListRestriction_internal
+
+pTerm7 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm7 = fmap snd . pTerm7_internal
+
+pTerm5 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm5 = fmap snd . pTerm5_internal
+
+pTerm4 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm4 = fmap snd . pTerm4_internal
+
+pTerm3 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm3 = fmap snd . pTerm3_internal
+
+pTerm2 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm2 = fmap snd . pTerm2_internal
+
+pTerm1 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm1 = fmap snd . pTerm1_internal
+
+pTerm6 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm6 = fmap snd . pTerm6_internal
+
+pTerm :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm = fmap snd . pTerm_internal
+
+pListTerm :: [Token] -> Err [Language.Rzk.Syntax.Abs.Term]
+pListTerm = fmap snd . pListTerm_internal
+}
+
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -107,8 +107,8 @@
         withCommand command $ do
           mapM_ checkDefinedVar (varIdentAt path <$> vars)
           paramDecls <- concat <$> mapM paramToParamDecl params
-          ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT -- >>= pure . termIsWHNF
-          term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT >>= pure . termIsWHNF
+          ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT
+          term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT
           let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars)
           fmap (decl :) $
             localDeclPrepared decl $ do
@@ -127,7 +127,7 @@
         withCommand command $ do
           mapM_ checkDefinedVar (varIdentAt path <$> vars)
           paramDecls <- concat <$> mapM paramToParamDecl params
-          ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT -- >>= pure . termIsWHNF
+          ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT
           let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars)
           fmap (decl :) $
             localDeclPrepared decl $
@@ -137,7 +137,7 @@
       traceTypeCheck Normal ("[ " <> show i <> " out of " <> show totalCommands <> " ]"
           <> " Checking " <> Rzk.printTree term <> " : " <> Rzk.printTree ty ) $ do
         withCommand command $ do
-          ty' <- typecheck (toTerm' ty) universeT >>= whnfT -- >>= pure . termIsWHNF
+          ty' <- typecheck (toTerm' ty) universeT >>= whnfT
           _term' <- typecheck (toTerm' term) ty'
           go (i + 1) moreCommands
 
@@ -1228,6 +1228,10 @@
 -- unit : Unit
 whnfT :: Eq var => TermT var -> TypeCheck var (TermT var)
 whnfT tt = performing (ActionWHNF tt) $ case tt of
+  -- use cached result if it exists
+  Free (AnnF info _)
+    | Just tt' <- infoWHNF info -> pure tt'
+
   -- universe constants
   UniverseT{} -> pure tt
   UniverseCubeT{} -> pure tt
@@ -1263,9 +1267,6 @@
   -- type ascriptions are ignored, since we already have a typechecked term
   TypeAscT _ty term _ty' -> whnfT term
 
-  Free (AnnF info _)
-    | Just tt' <- infoWHNF info -> pure tt'
-
   -- check if we have cube or a tope term (if so, compute NF)
   _ -> typeOf tt >>= \case
     UniverseCubeT{} -> nfTope tt
@@ -1281,7 +1282,7 @@
       UniverseCubeT{} -> nfTope tt
 
       -- now we are in the type layer
-      _ -> do
+      _ -> fmap termIsWHNF $ do
         -- check if we are in the empty context
         inBottom <- asks localTopesEntailBottom
         if inBottom
@@ -1618,9 +1619,16 @@
   where
     performUnification = unifyInCurrentContext mterm expected actual
 
+unifyViaDecompose :: Eq var => TermT var -> TermT var -> TypeCheck var ()
+unifyViaDecompose expected actual | expected == actual = return ()
+unifyViaDecompose (AppT _ f x) (AppT _ g y) = do
+  unify Nothing f g
+  unify Nothing x y
+unifyViaDecompose _ _ = issueTypeError (TypeErrorOther "cannot decompose")
+
 unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var ()
 unifyInCurrentContext mterm expected actual = performing action $
-  unless (expected == actual) $ do      -- NOTE: this gives a small, but noticeable speedup
+  unifyViaDecompose expected actual `catchError` \_ -> do      -- NOTE: this gives a small, but noticeable speedup
     expectedVal <- whnfT expected
     actualVal <- whnfT actual
     (expected', actual') <- asks covariance >>= \case