diff --git a/grammar.js b/grammar.js
index 938e017..d3f058c 100644
--- a/grammar.js
+++ b/grammar.js
@@ -17,12 +17,24 @@ module.exports = grammar({
 
   rules: {
 
-    program : $ => repeat(choice($.definition, $.preprocess, $.axiom)),
+    program : $ => repeat1(choice($.definition, $.preprocess, $.axiom, $.section, $.variable)),
 
     identifier : $ => /[a-zA-Z_]\w*/,
 
     comment : $ => token(seq('--', /.*/)),
 
+    section : $ => seq(
+      'section', $.identifier,
+      $.program,
+      'end', $.identifier,
+    ),
+
+    variable : $ => seq(
+      choice('variable', 'hypothesis'),
+      repeat1($.param_block),
+      ';'
+    ),
+
     param_block : $ => seq(
       '(',
       field('param', repeat1($.identifier)),
diff --git a/src/grammar.json b/src/grammar.json
index 83fa290..66a4de1 100644
--- a/src/grammar.json
+++ b/src/grammar.json
@@ -2,7 +2,7 @@
   "name": "perga",
   "rules": {
     "program": {
-      "type": "REPEAT",
+      "type": "REPEAT1",
       "content": {
         "type": "CHOICE",
         "members": [
@@ -17,6 +17,14 @@
           {
             "type": "SYMBOL",
             "name": "axiom"
+          },
+          {
+            "type": "SYMBOL",
+            "name": "section"
+          },
+          {
+            "type": "SYMBOL",
+            "name": "variable"
           }
         ]
       }
@@ -41,6 +49,60 @@
         ]
       }
     },
+    "section": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "section"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "program"
+        },
+        {
+          "type": "STRING",
+          "value": "end"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        }
+      ]
+    },
+    "variable": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "STRING",
+              "value": "variable"
+            },
+            {
+              "type": "STRING",
+              "value": "hypothesis"
+            }
+          ]
+        },
+        {
+          "type": "REPEAT1",
+          "content": {
+            "type": "SYMBOL",
+            "name": "param_block"
+          }
+        },
+        {
+          "type": "STRING",
+          "value": ";"
+        }
+      ]
+    },
     "param_block": {
       "type": "SEQ",
       "members": [
diff --git a/src/node-types.json b/src/node-types.json
index 7b03d9e..c63880e 100644
--- a/src/node-types.json
+++ b/src/node-types.json
@@ -302,7 +302,7 @@
     "fields": {},
     "children": {
       "multiple": true,
-      "required": false,
+      "required": true,
       "types": [
         {
           "type": "axiom",
@@ -315,6 +315,33 @@
         {
           "type": "preprocess",
           "named": true
+        },
+        {
+          "type": "section",
+          "named": true
+        },
+        {
+          "type": "variable",
+          "named": true
+        }
+      ]
+    }
+  },
+  {
+    "type": "section",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "identifier",
+          "named": true
+        },
+        {
+          "type": "program",
+          "named": true
         }
       ]
     }
@@ -366,6 +393,21 @@
       ]
     }
   },
+  {
+    "type": "variable",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "param_block",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "(",
     "named": false
@@ -430,6 +472,10 @@
     "type": "fun",
     "named": false
   },
+  {
+    "type": "hypothesis",
+    "named": false
+  },
   {
     "type": "identifier",
     "named": true
@@ -446,10 +492,18 @@
     "type": "post_command",
     "named": true
   },
+  {
+    "type": "section",
+    "named": false
+  },
   {
     "type": "star",
     "named": true
   },
+  {
+    "type": "variable",
+    "named": false
+  },
   {
     "type": "λ",
     "named": false
diff --git a/src/parser.c b/src/parser.c
index 0db4882..0098138 100644
--- a/src/parser.c
+++ b/src/parser.c
@@ -5,11 +5,11 @@
 #endif
 
 #define LANGUAGE_VERSION 14
-#define STATE_COUNT 108
+#define STATE_COUNT 149
 #define LARGE_STATE_COUNT 2
-#define SYMBOL_COUNT 50
+#define SYMBOL_COUNT 55
 #define ALIAS_COUNT 0
-#define TOKEN_COUNT 28
+#define TOKEN_COUNT 31
 #define EXTERNAL_TOKEN_COUNT 0
 #define FIELD_COUNT 3
 #define MAX_ALIAS_SEQUENCE_LENGTH 7
@@ -18,59 +18,69 @@
 enum ts_symbol_identifiers {
   sym_identifier = 1,
   sym_comment = 2,
-  anon_sym_LPAREN = 3,
-  anon_sym_COLON = 4,
-  anon_sym_RPAREN = 5,
-  sym_star = 6,
-  anon_sym_u25a1 = 7,
-  anon_sym_LBRACK_RBRACK = 8,
-  aux_sym_sort_token1 = 9,
-  anon_sym_u03bb = 10,
-  anon_sym_fun = 11,
-  anon_sym_EQ_GT = 12,
-  anon_sym_u21d2 = 13,
-  anon_sym_u220f = 14,
-  anon_sym_forall = 15,
-  anon_sym_COMMA = 16,
-  anon_sym_COLON_EQ = 17,
-  anon_sym_let = 18,
-  anon_sym_in = 19,
-  anon_sym_end = 20,
-  anon_sym_DASH_GT = 21,
-  anon_sym_u2192 = 22,
-  anon_sym_axiom = 23,
-  anon_sym_SEMI = 24,
-  anon_sym_def = 25,
-  sym_post_command = 26,
-  sym_command = 27,
-  sym_program = 28,
-  sym_param_block = 29,
-  sym_square = 30,
-  sym_sort = 31,
-  sym_labs = 32,
-  sym_pabs = 33,
-  sym_term = 34,
-  sym_binding = 35,
-  sym_let = 36,
-  sym_app = 37,
-  sym_arrow = 38,
-  sym_app_term = 39,
-  sym_expr = 40,
-  sym_ascription = 41,
-  sym_axiom = 42,
-  sym_definition = 43,
-  sym_preprocess = 44,
-  aux_sym_program_repeat1 = 45,
-  aux_sym_param_block_repeat1 = 46,
-  aux_sym_labs_repeat1 = 47,
-  aux_sym_let_repeat1 = 48,
-  aux_sym_app_repeat1 = 49,
+  anon_sym_section = 3,
+  anon_sym_end = 4,
+  anon_sym_variable = 5,
+  anon_sym_hypothesis = 6,
+  anon_sym_SEMI = 7,
+  anon_sym_LPAREN = 8,
+  anon_sym_COLON = 9,
+  anon_sym_RPAREN = 10,
+  sym_star = 11,
+  anon_sym_u25a1 = 12,
+  anon_sym_LBRACK_RBRACK = 13,
+  aux_sym_sort_token1 = 14,
+  anon_sym_u03bb = 15,
+  anon_sym_fun = 16,
+  anon_sym_EQ_GT = 17,
+  anon_sym_u21d2 = 18,
+  anon_sym_u220f = 19,
+  anon_sym_forall = 20,
+  anon_sym_COMMA = 21,
+  anon_sym_COLON_EQ = 22,
+  anon_sym_let = 23,
+  anon_sym_in = 24,
+  anon_sym_DASH_GT = 25,
+  anon_sym_u2192 = 26,
+  anon_sym_axiom = 27,
+  anon_sym_def = 28,
+  sym_post_command = 29,
+  sym_command = 30,
+  sym_program = 31,
+  sym_section = 32,
+  sym_variable = 33,
+  sym_param_block = 34,
+  sym_square = 35,
+  sym_sort = 36,
+  sym_labs = 37,
+  sym_pabs = 38,
+  sym_term = 39,
+  sym_binding = 40,
+  sym_let = 41,
+  sym_app = 42,
+  sym_arrow = 43,
+  sym_app_term = 44,
+  sym_expr = 45,
+  sym_ascription = 46,
+  sym_axiom = 47,
+  sym_definition = 48,
+  sym_preprocess = 49,
+  aux_sym_program_repeat1 = 50,
+  aux_sym_variable_repeat1 = 51,
+  aux_sym_param_block_repeat1 = 52,
+  aux_sym_let_repeat1 = 53,
+  aux_sym_app_repeat1 = 54,
 };
 
 static const char * const ts_symbol_names[] = {
   [ts_builtin_sym_end] = "end",
   [sym_identifier] = "identifier",
   [sym_comment] = "comment",
+  [anon_sym_section] = "section",
+  [anon_sym_end] = "end",
+  [anon_sym_variable] = "variable",
+  [anon_sym_hypothesis] = "hypothesis",
+  [anon_sym_SEMI] = ";",
   [anon_sym_LPAREN] = "(",
   [anon_sym_COLON] = ":",
   [anon_sym_RPAREN] = ")",
@@ -88,15 +98,15 @@ static const char * const ts_symbol_names[] = {
   [anon_sym_COLON_EQ] = ":=",
   [anon_sym_let] = "let",
   [anon_sym_in] = "in",
-  [anon_sym_end] = "end",
   [anon_sym_DASH_GT] = "->",
   [anon_sym_u2192] = "\u2192",
   [anon_sym_axiom] = "axiom",
-  [anon_sym_SEMI] = ";",
   [anon_sym_def] = "def",
   [sym_post_command] = "post_command",
   [sym_command] = "command",
   [sym_program] = "program",
+  [sym_section] = "section",
+  [sym_variable] = "variable",
   [sym_param_block] = "param_block",
   [sym_square] = "square",
   [sym_sort] = "sort",
@@ -114,8 +124,8 @@ static const char * const ts_symbol_names[] = {
   [sym_definition] = "definition",
   [sym_preprocess] = "preprocess",
   [aux_sym_program_repeat1] = "program_repeat1",
+  [aux_sym_variable_repeat1] = "variable_repeat1",
   [aux_sym_param_block_repeat1] = "param_block_repeat1",
-  [aux_sym_labs_repeat1] = "labs_repeat1",
   [aux_sym_let_repeat1] = "let_repeat1",
   [aux_sym_app_repeat1] = "app_repeat1",
 };
@@ -124,6 +134,11 @@ static const TSSymbol ts_symbol_map[] = {
   [ts_builtin_sym_end] = ts_builtin_sym_end,
   [sym_identifier] = sym_identifier,
   [sym_comment] = sym_comment,
+  [anon_sym_section] = anon_sym_section,
+  [anon_sym_end] = anon_sym_end,
+  [anon_sym_variable] = anon_sym_variable,
+  [anon_sym_hypothesis] = anon_sym_hypothesis,
+  [anon_sym_SEMI] = anon_sym_SEMI,
   [anon_sym_LPAREN] = anon_sym_LPAREN,
   [anon_sym_COLON] = anon_sym_COLON,
   [anon_sym_RPAREN] = anon_sym_RPAREN,
@@ -141,15 +156,15 @@ static const TSSymbol ts_symbol_map[] = {
   [anon_sym_COLON_EQ] = anon_sym_COLON_EQ,
   [anon_sym_let] = anon_sym_let,
   [anon_sym_in] = anon_sym_in,
-  [anon_sym_end] = anon_sym_end,
   [anon_sym_DASH_GT] = anon_sym_DASH_GT,
   [anon_sym_u2192] = anon_sym_u2192,
   [anon_sym_axiom] = anon_sym_axiom,
-  [anon_sym_SEMI] = anon_sym_SEMI,
   [anon_sym_def] = anon_sym_def,
   [sym_post_command] = sym_post_command,
   [sym_command] = sym_command,
   [sym_program] = sym_program,
+  [sym_section] = sym_section,
+  [sym_variable] = sym_variable,
   [sym_param_block] = sym_param_block,
   [sym_square] = sym_square,
   [sym_sort] = sym_sort,
@@ -167,8 +182,8 @@ static const TSSymbol ts_symbol_map[] = {
   [sym_definition] = sym_definition,
   [sym_preprocess] = sym_preprocess,
   [aux_sym_program_repeat1] = aux_sym_program_repeat1,
+  [aux_sym_variable_repeat1] = aux_sym_variable_repeat1,
   [aux_sym_param_block_repeat1] = aux_sym_param_block_repeat1,
-  [aux_sym_labs_repeat1] = aux_sym_labs_repeat1,
   [aux_sym_let_repeat1] = aux_sym_let_repeat1,
   [aux_sym_app_repeat1] = aux_sym_app_repeat1,
 };
@@ -186,6 +201,26 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = true,
   },
+  [anon_sym_section] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_end] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_variable] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_hypothesis] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_SEMI] = {
+    .visible = true,
+    .named = false,
+  },
   [anon_sym_LPAREN] = {
     .visible = true,
     .named = false,
@@ -254,10 +289,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
-  [anon_sym_end] = {
-    .visible = true,
-    .named = false,
-  },
   [anon_sym_DASH_GT] = {
     .visible = true,
     .named = false,
@@ -270,10 +301,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
-  [anon_sym_SEMI] = {
-    .visible = true,
-    .named = false,
-  },
   [anon_sym_def] = {
     .visible = true,
     .named = false,
@@ -290,6 +317,14 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = true,
   },
+  [sym_section] = {
+    .visible = true,
+    .named = true,
+  },
+  [sym_variable] = {
+    .visible = true,
+    .named = true,
+  },
   [sym_param_block] = {
     .visible = true,
     .named = true,
@@ -358,11 +393,11 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = false,
     .named = false,
   },
-  [aux_sym_param_block_repeat1] = {
+  [aux_sym_variable_repeat1] = {
     .visible = false,
     .named = false,
   },
-  [aux_sym_labs_repeat1] = {
+  [aux_sym_param_block_repeat1] = {
     .visible = false,
     .named = false,
   },
@@ -428,100 +463,141 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [11] = 11,
   [12] = 12,
   [13] = 13,
-  [14] = 3,
+  [14] = 14,
   [15] = 15,
-  [16] = 16,
-  [17] = 17,
-  [18] = 9,
-  [19] = 11,
-  [20] = 2,
-  [21] = 13,
-  [22] = 6,
-  [23] = 23,
-  [24] = 24,
-  [25] = 25,
+  [16] = 6,
+  [17] = 11,
+  [18] = 8,
+  [19] = 9,
+  [20] = 12,
+  [21] = 21,
+  [22] = 3,
+  [23] = 5,
+  [24] = 7,
+  [25] = 10,
   [26] = 26,
   [27] = 27,
   [28] = 28,
   [29] = 29,
   [30] = 30,
-  [31] = 24,
-  [32] = 23,
+  [31] = 31,
+  [32] = 32,
   [33] = 33,
   [34] = 34,
   [35] = 35,
-  [36] = 36,
-  [37] = 37,
+  [36] = 34,
+  [37] = 31,
   [38] = 38,
-  [39] = 39,
+  [39] = 30,
   [40] = 26,
-  [41] = 25,
+  [41] = 27,
   [42] = 42,
   [43] = 43,
   [44] = 44,
-  [45] = 28,
-  [46] = 30,
+  [45] = 45,
+  [46] = 29,
   [47] = 47,
-  [48] = 27,
-  [49] = 29,
+  [48] = 28,
+  [49] = 49,
   [50] = 50,
   [51] = 51,
-  [52] = 51,
+  [52] = 52,
   [53] = 53,
-  [54] = 54,
-  [55] = 55,
-  [56] = 56,
-  [57] = 57,
+  [54] = 32,
+  [55] = 38,
+  [56] = 33,
+  [57] = 35,
   [58] = 58,
-  [59] = 58,
+  [59] = 59,
   [60] = 60,
-  [61] = 61,
+  [61] = 59,
   [62] = 62,
   [63] = 63,
   [64] = 64,
   [65] = 65,
   [66] = 66,
-  [67] = 67,
-  [68] = 68,
+  [67] = 66,
+  [68] = 62,
   [69] = 69,
-  [70] = 70,
+  [70] = 58,
   [71] = 71,
-  [72] = 72,
-  [73] = 73,
-  [74] = 74,
-  [75] = 75,
-  [76] = 44,
-  [77] = 72,
-  [78] = 73,
+  [72] = 64,
+  [73] = 65,
+  [74] = 60,
+  [75] = 69,
+  [76] = 71,
+  [77] = 77,
+  [78] = 78,
   [79] = 79,
   [80] = 80,
-  [81] = 81,
+  [81] = 77,
   [82] = 82,
-  [83] = 83,
-  [84] = 83,
+  [83] = 80,
+  [84] = 79,
   [85] = 85,
   [86] = 86,
   [87] = 87,
-  [88] = 88,
-  [89] = 89,
+  [88] = 85,
+  [89] = 86,
   [90] = 90,
   [91] = 91,
-  [92] = 92,
+  [92] = 90,
   [93] = 93,
   [94] = 94,
   [95] = 95,
   [96] = 96,
   [97] = 97,
-  [98] = 98,
+  [98] = 53,
   [99] = 99,
-  [100] = 100,
+  [100] = 97,
   [101] = 101,
-  [102] = 102,
-  [103] = 100,
-  [104] = 97,
+  [102] = 95,
+  [103] = 94,
+  [104] = 104,
   [105] = 105,
   [106] = 106,
   [107] = 107,
+  [108] = 108,
+  [109] = 104,
+  [110] = 110,
+  [111] = 111,
+  [112] = 112,
+  [113] = 113,
+  [114] = 114,
+  [115] = 115,
+  [116] = 116,
+  [117] = 117,
+  [118] = 118,
+  [119] = 119,
+  [120] = 120,
+  [121] = 121,
+  [122] = 122,
+  [123] = 120,
+  [124] = 124,
+  [125] = 125,
+  [126] = 126,
+  [127] = 127,
+  [128] = 111,
+  [129] = 125,
+  [130] = 130,
+  [131] = 121,
+  [132] = 132,
+  [133] = 133,
+  [134] = 132,
+  [135] = 122,
+  [136] = 136,
+  [137] = 137,
+  [138] = 116,
+  [139] = 119,
+  [140] = 115,
+  [141] = 141,
+  [142] = 142,
+  [143] = 136,
+  [144] = 118,
+  [145] = 113,
+  [146] = 130,
+  [147] = 110,
+  [148] = 124,
 };
 
 static bool ts_lex(TSLexer *lexer, TSStateId state) {
@@ -529,402 +605,480 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
   eof = lexer->eof(lexer);
   switch (state) {
     case 0:
-      if (eof) ADVANCE(33);
+      if (eof) ADVANCE(55);
       ADVANCE_MAP(
-        '(', 46,
-        ')', 48,
-        '*', 49,
-        ',', 61,
+        '(', 74,
+        ')', 76,
+        '*', 77,
+        ',', 89,
         '-', 6,
-        ':', 47,
-        ';', 71,
+        ':', 75,
+        ';', 73,
         '=', 7,
-        '@', 18,
+        '@', 27,
         '[', 8,
-        'a', 32,
-        'd', 13,
-        'e', 23,
-        'f', 27,
-        'i', 24,
-        'l', 14,
-        0x3bb, 53,
-        0x2192, 69,
-        0x21d2, 57,
-        0x220f, 58,
-        0x25a1, 50,
+        'a', 53,
+        'd', 17,
+        'e', 35,
+        'f', 40,
+        'h', 54,
+        'i', 36,
+        'l', 18,
+        's', 19,
+        'v', 10,
+        0x3bb, 81,
+        0x2192, 95,
+        0x21d2, 85,
+        0x220f, 86,
+        0x25a1, 78,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(0);
       if (('0' <= lookahead && lookahead <= '9') ||
-          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(52);
+          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(80);
       END_STATE();
     case 1:
       if (lookahead == '\n') SKIP(1);
-      if (lookahead == '-') ADVANCE(73);
+      if (lookahead == '-') ADVANCE(98);
       if (('\t' <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') ADVANCE(74);
-      if (lookahead != 0) ADVANCE(75);
+          lookahead == ' ') ADVANCE(99);
+      if (lookahead != 0) ADVANCE(100);
       END_STATE();
     case 2:
       ADVANCE_MAP(
-        '(', 46,
-        ')', 48,
-        '*', 49,
-        ',', 61,
+        '(', 74,
+        ')', 76,
+        '*', 77,
+        ',', 89,
         '-', 6,
-        ':', 47,
-        ';', 71,
+        ':', 75,
+        ';', 73,
         '=', 7,
         '[', 8,
-        0x2192, 69,
-        0x21d2, 57,
-        0x25a1, 50,
+        0x2192, 95,
+        0x21d2, 85,
+        0x25a1, 78,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(2);
       if (('0' <= lookahead && lookahead <= '9') ||
-          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(52);
+          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(80);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
       END_STATE();
     case 3:
-      if (lookahead == '(') ADVANCE(46);
-      if (lookahead == '*') ADVANCE(49);
+      if (lookahead == '(') ADVANCE(74);
+      if (lookahead == '*') ADVANCE(77);
       if (lookahead == '-') ADVANCE(6);
       if (lookahead == '[') ADVANCE(8);
-      if (lookahead == 'e') ADVANCE(40);
-      if (lookahead == 0x2192) ADVANCE(69);
-      if (lookahead == 0x25a1) ADVANCE(50);
+      if (lookahead == 'e') ADVANCE(62);
+      if (lookahead == 0x2192) ADVANCE(95);
+      if (lookahead == 0x25a1) ADVANCE(78);
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(3);
       if (('0' <= lookahead && lookahead <= '9') ||
-          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(52);
+          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(80);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
       END_STATE();
     case 4:
       ADVANCE_MAP(
-        '(', 46,
-        '*', 49,
+        '(', 74,
+        '*', 77,
         '-', 5,
         '[', 8,
-        'f', 41,
-        'l', 36,
-        0x3bb, 53,
-        0x220f, 58,
-        0x25a1, 50,
+        'f', 63,
+        'l', 58,
+        0x3bb, 81,
+        0x220f, 86,
+        0x25a1, 78,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(4);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
       END_STATE();
     case 5:
-      if (lookahead == '-') ADVANCE(45);
+      if (lookahead == '-') ADVANCE(67);
       END_STATE();
     case 6:
-      if (lookahead == '-') ADVANCE(45);
-      if (lookahead == '>') ADVANCE(68);
+      if (lookahead == '-') ADVANCE(67);
+      if (lookahead == '>') ADVANCE(94);
       END_STATE();
     case 7:
-      if (lookahead == '>') ADVANCE(56);
+      if (lookahead == '>') ADVANCE(84);
       END_STATE();
     case 8:
-      if (lookahead == ']') ADVANCE(51);
+      if (lookahead == ']') ADVANCE(79);
       END_STATE();
     case 9:
-      if (lookahead == 'a') ADVANCE(21);
+      if (lookahead == 'a') ADVANCE(12);
       END_STATE();
     case 10:
-      if (lookahead == 'c') ADVANCE(19);
+      if (lookahead == 'a') ADVANCE(46);
       END_STATE();
     case 11:
-      if (lookahead == 'd') ADVANCE(66);
+      if (lookahead == 'a') ADVANCE(32);
       END_STATE();
     case 12:
-      if (lookahead == 'd') ADVANCE(15);
+      if (lookahead == 'b') ADVANCE(33);
       END_STATE();
     case 13:
-      if (lookahead == 'e') ADVANCE(16);
+      if (lookahead == 'c') ADVANCE(30);
       END_STATE();
     case 14:
-      if (lookahead == 'e') ADVANCE(30);
+      if (lookahead == 'c') ADVANCE(51);
       END_STATE();
     case 15:
-      if (lookahead == 'e') ADVANCE(76);
+      if (lookahead == 'd') ADVANCE(69);
       END_STATE();
     case 16:
-      if (lookahead == 'f') ADVANCE(72);
+      if (lookahead == 'd') ADVANCE(21);
       END_STATE();
     case 17:
-      if (lookahead == 'i') ADVANCE(28);
+      if (lookahead == 'e') ADVANCE(23);
       END_STATE();
     case 18:
-      if (lookahead == 'i') ADVANCE(25);
+      if (lookahead == 'e') ADVANCE(49);
       END_STATE();
     case 19:
-      if (lookahead == 'l') ADVANCE(31);
+      if (lookahead == 'e') ADVANCE(14);
       END_STATE();
     case 20:
-      if (lookahead == 'l') ADVANCE(59);
+      if (lookahead == 'e') ADVANCE(48);
       END_STATE();
     case 21:
-      if (lookahead == 'l') ADVANCE(20);
+      if (lookahead == 'e') ADVANCE(101);
       END_STATE();
     case 22:
-      if (lookahead == 'm') ADVANCE(70);
+      if (lookahead == 'e') ADVANCE(71);
       END_STATE();
     case 23:
-      if (lookahead == 'n') ADVANCE(11);
+      if (lookahead == 'f') ADVANCE(97);
       END_STATE();
     case 24:
-      if (lookahead == 'n') ADVANCE(65);
+      if (lookahead == 'h') ADVANCE(20);
       END_STATE();
     case 25:
-      if (lookahead == 'n') ADVANCE(10);
+      if (lookahead == 'i') ADVANCE(41);
       END_STATE();
     case 26:
-      if (lookahead == 'n') ADVANCE(54);
+      if (lookahead == 'i') ADVANCE(47);
       END_STATE();
     case 27:
-      if (lookahead == 'o') ADVANCE(29);
-      if (lookahead == 'u') ADVANCE(26);
+      if (lookahead == 'i') ADVANCE(39);
       END_STATE();
     case 28:
-      if (lookahead == 'o') ADVANCE(22);
+      if (lookahead == 'i') ADVANCE(9);
       END_STATE();
     case 29:
-      if (lookahead == 'r') ADVANCE(9);
+      if (lookahead == 'i') ADVANCE(43);
       END_STATE();
     case 30:
-      if (lookahead == 't') ADVANCE(63);
+      if (lookahead == 'l') ADVANCE(52);
       END_STATE();
     case 31:
-      if (lookahead == 'u') ADVANCE(12);
+      if (lookahead == 'l') ADVANCE(87);
       END_STATE();
     case 32:
-      if (lookahead == 'x') ADVANCE(17);
+      if (lookahead == 'l') ADVANCE(31);
       END_STATE();
     case 33:
-      ACCEPT_TOKEN(ts_builtin_sym_end);
+      if (lookahead == 'l') ADVANCE(22);
       END_STATE();
     case 34:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'a') ADVANCE(38);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('b' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'm') ADVANCE(96);
       END_STATE();
     case 35:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'd') ADVANCE(67);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'n') ADVANCE(15);
       END_STATE();
     case 36:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'e') ADVANCE(43);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'n') ADVANCE(93);
       END_STATE();
     case 37:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'l') ADVANCE(60);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'n') ADVANCE(82);
       END_STATE();
     case 38:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'l') ADVANCE(37);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'n') ADVANCE(68);
       END_STATE();
     case 39:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'n') ADVANCE(55);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'n') ADVANCE(13);
       END_STATE();
     case 40:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'n') ADVANCE(35);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'o') ADVANCE(45);
+      if (lookahead == 'u') ADVANCE(37);
       END_STATE();
     case 41:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'o') ADVANCE(42);
-      if (lookahead == 'u') ADVANCE(39);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'o') ADVANCE(34);
       END_STATE();
     case 42:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'r') ADVANCE(34);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'o') ADVANCE(50);
       END_STATE();
     case 43:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 't') ADVANCE(64);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
+      if (lookahead == 'o') ADVANCE(38);
       END_STATE();
     case 44:
+      if (lookahead == 'p') ADVANCE(42);
+      END_STATE();
+    case 45:
+      if (lookahead == 'r') ADVANCE(11);
+      END_STATE();
+    case 46:
+      if (lookahead == 'r') ADVANCE(28);
+      END_STATE();
+    case 47:
+      if (lookahead == 's') ADVANCE(72);
+      END_STATE();
+    case 48:
+      if (lookahead == 's') ADVANCE(26);
+      END_STATE();
+    case 49:
+      if (lookahead == 't') ADVANCE(91);
+      END_STATE();
+    case 50:
+      if (lookahead == 't') ADVANCE(24);
+      END_STATE();
+    case 51:
+      if (lookahead == 't') ADVANCE(29);
+      END_STATE();
+    case 52:
+      if (lookahead == 'u') ADVANCE(16);
+      END_STATE();
+    case 53:
+      if (lookahead == 'x') ADVANCE(25);
+      END_STATE();
+    case 54:
+      if (lookahead == 'y') ADVANCE(44);
+      END_STATE();
+    case 55:
+      ACCEPT_TOKEN(ts_builtin_sym_end);
+      END_STATE();
+    case 56:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'a') ADVANCE(60);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('b' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 57:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'd') ADVANCE(70);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 58:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'e') ADVANCE(65);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 59:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'l') ADVANCE(88);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 60:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'l') ADVANCE(59);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 61:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'n') ADVANCE(83);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 62:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'n') ADVANCE(57);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 63:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'o') ADVANCE(64);
+      if (lookahead == 'u') ADVANCE(61);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 64:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'r') ADVANCE(56);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 65:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 't') ADVANCE(92);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 66:
       ACCEPT_TOKEN(sym_identifier);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
-      END_STATE();
-    case 45:
-      ACCEPT_TOKEN(sym_comment);
-      if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(45);
-      END_STATE();
-    case 46:
-      ACCEPT_TOKEN(anon_sym_LPAREN);
-      END_STATE();
-    case 47:
-      ACCEPT_TOKEN(anon_sym_COLON);
-      if (lookahead == '=') ADVANCE(62);
-      END_STATE();
-    case 48:
-      ACCEPT_TOKEN(anon_sym_RPAREN);
-      END_STATE();
-    case 49:
-      ACCEPT_TOKEN(sym_star);
-      END_STATE();
-    case 50:
-      ACCEPT_TOKEN(anon_sym_u25a1);
-      END_STATE();
-    case 51:
-      ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK);
-      END_STATE();
-    case 52:
-      ACCEPT_TOKEN(aux_sym_sort_token1);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(52);
-      END_STATE();
-    case 53:
-      ACCEPT_TOKEN(anon_sym_u03bb);
-      END_STATE();
-    case 54:
-      ACCEPT_TOKEN(anon_sym_fun);
-      END_STATE();
-    case 55:
-      ACCEPT_TOKEN(anon_sym_fun);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
-      END_STATE();
-    case 56:
-      ACCEPT_TOKEN(anon_sym_EQ_GT);
-      END_STATE();
-    case 57:
-      ACCEPT_TOKEN(anon_sym_u21d2);
-      END_STATE();
-    case 58:
-      ACCEPT_TOKEN(anon_sym_u220f);
-      END_STATE();
-    case 59:
-      ACCEPT_TOKEN(anon_sym_forall);
-      END_STATE();
-    case 60:
-      ACCEPT_TOKEN(anon_sym_forall);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
-      END_STATE();
-    case 61:
-      ACCEPT_TOKEN(anon_sym_COMMA);
-      END_STATE();
-    case 62:
-      ACCEPT_TOKEN(anon_sym_COLON_EQ);
-      END_STATE();
-    case 63:
-      ACCEPT_TOKEN(anon_sym_let);
-      END_STATE();
-    case 64:
-      ACCEPT_TOKEN(anon_sym_let);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
-      END_STATE();
-    case 65:
-      ACCEPT_TOKEN(anon_sym_in);
-      END_STATE();
-    case 66:
-      ACCEPT_TOKEN(anon_sym_end);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
       END_STATE();
     case 67:
+      ACCEPT_TOKEN(sym_comment);
+      if (lookahead != 0 &&
+          lookahead != '\n') ADVANCE(67);
+      END_STATE();
+    case 68:
+      ACCEPT_TOKEN(anon_sym_section);
+      END_STATE();
+    case 69:
+      ACCEPT_TOKEN(anon_sym_end);
+      END_STATE();
+    case 70:
       ACCEPT_TOKEN(anon_sym_end);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
-      END_STATE();
-    case 68:
-      ACCEPT_TOKEN(anon_sym_DASH_GT);
-      END_STATE();
-    case 69:
-      ACCEPT_TOKEN(anon_sym_u2192);
-      END_STATE();
-    case 70:
-      ACCEPT_TOKEN(anon_sym_axiom);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
       END_STATE();
     case 71:
-      ACCEPT_TOKEN(anon_sym_SEMI);
+      ACCEPT_TOKEN(anon_sym_variable);
       END_STATE();
     case 72:
-      ACCEPT_TOKEN(anon_sym_def);
+      ACCEPT_TOKEN(anon_sym_hypothesis);
       END_STATE();
     case 73:
-      ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '-') ADVANCE(45);
-      if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(75);
+      ACCEPT_TOKEN(anon_sym_SEMI);
       END_STATE();
     case 74:
-      ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '-') ADVANCE(73);
-      if (lookahead == '\t' ||
-          (0x0b <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') ADVANCE(74);
-      if (lookahead != 0 &&
-          (lookahead < '\t' || '\r' < lookahead)) ADVANCE(75);
+      ACCEPT_TOKEN(anon_sym_LPAREN);
       END_STATE();
     case 75:
-      ACCEPT_TOKEN(sym_post_command);
-      if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(75);
+      ACCEPT_TOKEN(anon_sym_COLON);
+      if (lookahead == '=') ADVANCE(90);
       END_STATE();
     case 76:
+      ACCEPT_TOKEN(anon_sym_RPAREN);
+      END_STATE();
+    case 77:
+      ACCEPT_TOKEN(sym_star);
+      END_STATE();
+    case 78:
+      ACCEPT_TOKEN(anon_sym_u25a1);
+      END_STATE();
+    case 79:
+      ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK);
+      END_STATE();
+    case 80:
+      ACCEPT_TOKEN(aux_sym_sort_token1);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          (0x2080 <= lookahead && lookahead <= 0x2089)) ADVANCE(80);
+      END_STATE();
+    case 81:
+      ACCEPT_TOKEN(anon_sym_u03bb);
+      END_STATE();
+    case 82:
+      ACCEPT_TOKEN(anon_sym_fun);
+      END_STATE();
+    case 83:
+      ACCEPT_TOKEN(anon_sym_fun);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 84:
+      ACCEPT_TOKEN(anon_sym_EQ_GT);
+      END_STATE();
+    case 85:
+      ACCEPT_TOKEN(anon_sym_u21d2);
+      END_STATE();
+    case 86:
+      ACCEPT_TOKEN(anon_sym_u220f);
+      END_STATE();
+    case 87:
+      ACCEPT_TOKEN(anon_sym_forall);
+      END_STATE();
+    case 88:
+      ACCEPT_TOKEN(anon_sym_forall);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 89:
+      ACCEPT_TOKEN(anon_sym_COMMA);
+      END_STATE();
+    case 90:
+      ACCEPT_TOKEN(anon_sym_COLON_EQ);
+      END_STATE();
+    case 91:
+      ACCEPT_TOKEN(anon_sym_let);
+      END_STATE();
+    case 92:
+      ACCEPT_TOKEN(anon_sym_let);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(66);
+      END_STATE();
+    case 93:
+      ACCEPT_TOKEN(anon_sym_in);
+      END_STATE();
+    case 94:
+      ACCEPT_TOKEN(anon_sym_DASH_GT);
+      END_STATE();
+    case 95:
+      ACCEPT_TOKEN(anon_sym_u2192);
+      END_STATE();
+    case 96:
+      ACCEPT_TOKEN(anon_sym_axiom);
+      END_STATE();
+    case 97:
+      ACCEPT_TOKEN(anon_sym_def);
+      END_STATE();
+    case 98:
+      ACCEPT_TOKEN(sym_post_command);
+      if (lookahead == '-') ADVANCE(67);
+      if (lookahead != 0 &&
+          lookahead != '\n') ADVANCE(100);
+      END_STATE();
+    case 99:
+      ACCEPT_TOKEN(sym_post_command);
+      if (lookahead == '-') ADVANCE(98);
+      if (lookahead == '\t' ||
+          (0x0b <= lookahead && lookahead <= '\r') ||
+          lookahead == ' ') ADVANCE(99);
+      if (lookahead != 0 &&
+          (lookahead < '\t' || '\r' < lookahead)) ADVANCE(100);
+      END_STATE();
+    case 100:
+      ACCEPT_TOKEN(sym_post_command);
+      if (lookahead != 0 &&
+          lookahead != '\n') ADVANCE(100);
+      END_STATE();
+    case 101:
       ACCEPT_TOKEN(sym_command);
       END_STATE();
     default:
@@ -956,41 +1110,41 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [20] = {.lex_state = 4},
   [21] = {.lex_state = 4},
   [22] = {.lex_state = 4},
-  [23] = {.lex_state = 2},
-  [24] = {.lex_state = 2},
-  [25] = {.lex_state = 2},
+  [23] = {.lex_state = 4},
+  [24] = {.lex_state = 4},
+  [25] = {.lex_state = 4},
   [26] = {.lex_state = 2},
   [27] = {.lex_state = 2},
   [28] = {.lex_state = 2},
   [29] = {.lex_state = 2},
-  [30] = {.lex_state = 2},
-  [31] = {.lex_state = 3},
-  [32] = {.lex_state = 3},
-  [33] = {.lex_state = 0},
+  [30] = {.lex_state = 0},
+  [31] = {.lex_state = 0},
+  [32] = {.lex_state = 2},
+  [33] = {.lex_state = 2},
   [34] = {.lex_state = 0},
-  [35] = {.lex_state = 0},
+  [35] = {.lex_state = 2},
   [36] = {.lex_state = 0},
   [37] = {.lex_state = 0},
-  [38] = {.lex_state = 0},
+  [38] = {.lex_state = 2},
   [39] = {.lex_state = 0},
   [40] = {.lex_state = 3},
   [41] = {.lex_state = 3},
   [42] = {.lex_state = 0},
   [43] = {.lex_state = 0},
   [44] = {.lex_state = 0},
-  [45] = {.lex_state = 3},
+  [45] = {.lex_state = 0},
   [46] = {.lex_state = 3},
   [47] = {.lex_state = 0},
   [48] = {.lex_state = 3},
-  [49] = {.lex_state = 3},
+  [49] = {.lex_state = 0},
   [50] = {.lex_state = 0},
   [51] = {.lex_state = 0},
   [52] = {.lex_state = 0},
   [53] = {.lex_state = 0},
-  [54] = {.lex_state = 0},
-  [55] = {.lex_state = 0},
-  [56] = {.lex_state = 0},
-  [57] = {.lex_state = 0},
+  [54] = {.lex_state = 3},
+  [55] = {.lex_state = 3},
+  [56] = {.lex_state = 3},
+  [57] = {.lex_state = 3},
   [58] = {.lex_state = 0},
   [59] = {.lex_state = 0},
   [60] = {.lex_state = 0},
@@ -1004,18 +1158,18 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [68] = {.lex_state = 0},
   [69] = {.lex_state = 0},
   [70] = {.lex_state = 0},
-  [71] = {.lex_state = 2},
+  [71] = {.lex_state = 0},
   [72] = {.lex_state = 0},
   [73] = {.lex_state = 0},
   [74] = {.lex_state = 0},
-  [75] = {.lex_state = 2},
+  [75] = {.lex_state = 0},
   [76] = {.lex_state = 0},
   [77] = {.lex_state = 0},
   [78] = {.lex_state = 0},
   [79] = {.lex_state = 0},
   [80] = {.lex_state = 0},
   [81] = {.lex_state = 0},
-  [82] = {.lex_state = 2},
+  [82] = {.lex_state = 0},
   [83] = {.lex_state = 0},
   [84] = {.lex_state = 0},
   [85] = {.lex_state = 0},
@@ -1024,29 +1178,75 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [88] = {.lex_state = 0},
   [89] = {.lex_state = 0},
   [90] = {.lex_state = 0},
-  [91] = {.lex_state = 2},
+  [91] = {.lex_state = 0},
   [92] = {.lex_state = 0},
   [93] = {.lex_state = 0},
-  [94] = {.lex_state = 2},
+  [94] = {.lex_state = 0},
   [95] = {.lex_state = 0},
   [96] = {.lex_state = 2},
   [97] = {.lex_state = 0},
   [98] = {.lex_state = 0},
-  [99] = {.lex_state = 0},
+  [99] = {.lex_state = 2},
   [100] = {.lex_state = 0},
-  [101] = {.lex_state = 1},
+  [101] = {.lex_state = 0},
   [102] = {.lex_state = 0},
   [103] = {.lex_state = 0},
   [104] = {.lex_state = 0},
-  [105] = {.lex_state = 0},
+  [105] = {.lex_state = 2},
   [106] = {.lex_state = 0},
   [107] = {.lex_state = 0},
+  [108] = {.lex_state = 0},
+  [109] = {.lex_state = 0},
+  [110] = {.lex_state = 2},
+  [111] = {.lex_state = 0},
+  [112] = {.lex_state = 0},
+  [113] = {.lex_state = 0},
+  [114] = {.lex_state = 0},
+  [115] = {.lex_state = 2},
+  [116] = {.lex_state = 1},
+  [117] = {.lex_state = 0},
+  [118] = {.lex_state = 0},
+  [119] = {.lex_state = 2},
+  [120] = {.lex_state = 0},
+  [121] = {.lex_state = 0},
+  [122] = {.lex_state = 0},
+  [123] = {.lex_state = 0},
+  [124] = {.lex_state = 0},
+  [125] = {.lex_state = 0},
+  [126] = {.lex_state = 0},
+  [127] = {.lex_state = 0},
+  [128] = {.lex_state = 0},
+  [129] = {.lex_state = 0},
+  [130] = {.lex_state = 2},
+  [131] = {.lex_state = 0},
+  [132] = {.lex_state = 0},
+  [133] = {.lex_state = 2},
+  [134] = {.lex_state = 0},
+  [135] = {.lex_state = 0},
+  [136] = {.lex_state = 0},
+  [137] = {.lex_state = 0},
+  [138] = {.lex_state = 1},
+  [139] = {.lex_state = 2},
+  [140] = {.lex_state = 2},
+  [141] = {.lex_state = 0},
+  [142] = {.lex_state = 0},
+  [143] = {.lex_state = 0},
+  [144] = {.lex_state = 0},
+  [145] = {.lex_state = 0},
+  [146] = {.lex_state = 2},
+  [147] = {.lex_state = 2},
+  [148] = {.lex_state = 0},
 };
 
 static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
   [0] = {
     [ts_builtin_sym_end] = ACTIONS(1),
     [sym_comment] = ACTIONS(3),
+    [anon_sym_section] = ACTIONS(1),
+    [anon_sym_end] = ACTIONS(1),
+    [anon_sym_variable] = ACTIONS(1),
+    [anon_sym_hypothesis] = ACTIONS(1),
+    [anon_sym_SEMI] = ACTIONS(1),
     [anon_sym_LPAREN] = ACTIONS(1),
     [anon_sym_COLON] = ACTIONS(1),
     [anon_sym_RPAREN] = ACTIONS(1),
@@ -1064,25 +1264,27 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
     [anon_sym_COLON_EQ] = ACTIONS(1),
     [anon_sym_let] = ACTIONS(1),
     [anon_sym_in] = ACTIONS(1),
-    [anon_sym_end] = ACTIONS(1),
     [anon_sym_DASH_GT] = ACTIONS(1),
     [anon_sym_u2192] = ACTIONS(1),
     [anon_sym_axiom] = ACTIONS(1),
-    [anon_sym_SEMI] = ACTIONS(1),
     [anon_sym_def] = ACTIONS(1),
     [sym_command] = ACTIONS(1),
   },
   [1] = {
-    [sym_program] = STATE(99),
-    [sym_axiom] = STATE(43),
-    [sym_definition] = STATE(43),
-    [sym_preprocess] = STATE(43),
-    [aux_sym_program_repeat1] = STATE(43),
-    [ts_builtin_sym_end] = ACTIONS(5),
+    [sym_program] = STATE(141),
+    [sym_section] = STATE(36),
+    [sym_variable] = STATE(36),
+    [sym_axiom] = STATE(36),
+    [sym_definition] = STATE(36),
+    [sym_preprocess] = STATE(36),
+    [aux_sym_program_repeat1] = STATE(36),
     [sym_comment] = ACTIONS(3),
-    [anon_sym_axiom] = ACTIONS(7),
-    [anon_sym_def] = ACTIONS(9),
-    [sym_command] = ACTIONS(11),
+    [anon_sym_section] = ACTIONS(5),
+    [anon_sym_variable] = ACTIONS(7),
+    [anon_sym_hypothesis] = ACTIONS(7),
+    [anon_sym_axiom] = ACTIONS(9),
+    [anon_sym_def] = ACTIONS(11),
+    [sym_command] = ACTIONS(13),
   },
 };
 
@@ -1090,39 +1292,39 @@ static const uint16_t ts_small_parse_table[] = {
   [0] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
     ACTIONS(15), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(17), 1,
+      anon_sym_LPAREN,
+    ACTIONS(19), 1,
       sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
     ACTIONS(23), 1,
-      anon_sym_fun,
+      anon_sym_u03bb,
     ACTIONS(25), 1,
-      anon_sym_u220f,
+      anon_sym_fun,
     ACTIONS(27), 1,
-      anon_sym_forall,
+      anon_sym_u220f,
     ACTIONS(29), 1,
+      anon_sym_forall,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    STATE(46), 1,
       sym_square,
-    STATE(28), 1,
-      sym_sort,
-    STATE(35), 1,
-      sym_expr,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(56), 1,
+      sym_sort,
+    STATE(98), 1,
       sym_app_term,
-    ACTIONS(19), 2,
+    STATE(112), 1,
+      sym_expr,
+    ACTIONS(21), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(41), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1130,39 +1332,39 @@ static const uint16_t ts_small_parse_table[] = {
   [57] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
     ACTIONS(31), 1,
-      sym_identifier,
+      anon_sym_let,
     ACTIONS(33), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
       sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
     ACTIONS(41), 1,
-      anon_sym_fun,
+      anon_sym_u03bb,
     ACTIONS(43), 1,
-      anon_sym_u220f,
+      anon_sym_fun,
     ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
       anon_sym_forall,
-    STATE(37), 1,
-      sym_expr,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(41), 1,
+    STATE(29), 1,
       sym_square,
-    STATE(45), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(76), 1,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(53), 1,
       sym_app_term,
-    ACTIONS(37), 2,
+    STATE(135), 1,
+      sym_expr,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(31), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1170,39 +1372,39 @@ static const uint16_t ts_small_parse_table[] = {
   [114] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    STATE(62), 1,
+    STATE(117), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1210,39 +1412,39 @@ static const uint16_t ts_small_parse_table[] = {
   [171] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    STATE(86), 1,
+    STATE(120), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1250,39 +1452,39 @@ static const uint16_t ts_small_parse_table[] = {
   [228] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(103), 1,
+    STATE(50), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    STATE(53), 1,
+      sym_app_term,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1290,39 +1492,39 @@ static const uint16_t ts_small_parse_table[] = {
   [285] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    STATE(90), 1,
+    STATE(124), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1330,39 +1532,39 @@ static const uint16_t ts_small_parse_table[] = {
   [342] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(92), 1,
+    STATE(51), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    STATE(53), 1,
+      sym_app_term,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1370,39 +1572,39 @@ static const uint16_t ts_small_parse_table[] = {
   [399] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
-      sym_sort,
     STATE(33), 1,
+      sym_sort,
+    STATE(43), 1,
       sym_expr,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1410,39 +1612,39 @@ static const uint16_t ts_small_parse_table[] = {
   [456] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    STATE(98), 1,
+    STATE(125), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1450,39 +1652,39 @@ static const uint16_t ts_small_parse_table[] = {
   [513] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(34), 1,
+    STATE(47), 1,
       sym_expr,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1490,39 +1692,39 @@ static const uint16_t ts_small_parse_table[] = {
   [570] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
     ACTIONS(31), 1,
-      sym_identifier,
+      anon_sym_let,
     ACTIONS(33), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
       sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
     ACTIONS(41), 1,
-      anon_sym_fun,
+      anon_sym_u03bb,
     ACTIONS(43), 1,
-      anon_sym_u220f,
+      anon_sym_fun,
     ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
       anon_sym_forall,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(41), 1,
+    STATE(29), 1,
       sym_square,
-    STATE(45), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(76), 1,
-      sym_app_term,
-    STATE(107), 1,
+    STATE(42), 1,
       sym_expr,
-    ACTIONS(37), 2,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(53), 1,
+      sym_app_term,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(31), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1530,39 +1732,39 @@ static const uint16_t ts_small_parse_table[] = {
   [627] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(39), 1,
-      sym_expr,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    ACTIONS(19), 2,
+    STATE(137), 1,
+      sym_expr,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1570,39 +1772,39 @@ static const uint16_t ts_small_parse_table[] = {
   [684] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(37), 1,
-      sym_expr,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    ACTIONS(19), 2,
+    STATE(142), 1,
+      sym_expr,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1610,39 +1812,39 @@ static const uint16_t ts_small_parse_table[] = {
   [741] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    STATE(93), 1,
+    STATE(114), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1650,39 +1852,39 @@ static const uint16_t ts_small_parse_table[] = {
   [798] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
     ACTIONS(15), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(17), 1,
+      anon_sym_LPAREN,
+    ACTIONS(19), 1,
       sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
     ACTIONS(23), 1,
-      anon_sym_fun,
+      anon_sym_u03bb,
     ACTIONS(25), 1,
-      anon_sym_u220f,
+      anon_sym_fun,
     ACTIONS(27), 1,
-      anon_sym_forall,
+      anon_sym_u220f,
     ACTIONS(29), 1,
+      anon_sym_forall,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    STATE(46), 1,
       sym_square,
-    STATE(28), 1,
-      sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(85), 1,
+    STATE(50), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    STATE(56), 1,
+      sym_sort,
+    STATE(98), 1,
+      sym_app_term,
+    ACTIONS(21), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(41), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1690,39 +1892,39 @@ static const uint16_t ts_small_parse_table[] = {
   [855] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
     ACTIONS(15), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(17), 1,
+      anon_sym_LPAREN,
+    ACTIONS(19), 1,
       sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
     ACTIONS(23), 1,
-      anon_sym_fun,
+      anon_sym_u03bb,
     ACTIONS(25), 1,
-      anon_sym_u220f,
+      anon_sym_fun,
     ACTIONS(27), 1,
-      anon_sym_forall,
+      anon_sym_u220f,
     ACTIONS(29), 1,
+      anon_sym_forall,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    STATE(46), 1,
       sym_square,
-    STATE(28), 1,
-      sym_sort,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(106), 1,
+    STATE(47), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(56), 1,
+      sym_sort,
+    STATE(98), 1,
+      sym_app_term,
+    ACTIONS(21), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(41), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1730,39 +1932,39 @@ static const uint16_t ts_small_parse_table[] = {
   [912] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
-    ACTIONS(31), 1,
+    ACTIONS(15), 1,
       sym_identifier,
-    ACTIONS(33), 1,
+    ACTIONS(17), 1,
       anon_sym_LPAREN,
-    ACTIONS(35), 1,
+    ACTIONS(19), 1,
       sym_star,
-    ACTIONS(39), 1,
+    ACTIONS(23), 1,
       anon_sym_u03bb,
-    ACTIONS(41), 1,
+    ACTIONS(25), 1,
       anon_sym_fun,
-    ACTIONS(43), 1,
+    ACTIONS(27), 1,
       anon_sym_u220f,
-    ACTIONS(45), 1,
+    ACTIONS(29), 1,
       anon_sym_forall,
-    STATE(33), 1,
-      sym_expr,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(41), 1,
+    ACTIONS(31), 1,
+      anon_sym_let,
+    STATE(46), 1,
       sym_square,
-    STATE(45), 1,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(51), 1,
+      sym_expr,
+    STATE(56), 1,
       sym_sort,
-    STATE(76), 1,
+    STATE(98), 1,
       sym_app_term,
-    ACTIONS(37), 2,
+    ACTIONS(21), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(31), 2,
+    STATE(41), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1770,39 +1972,39 @@ static const uint16_t ts_small_parse_table[] = {
   [969] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
-    ACTIONS(31), 1,
+    ACTIONS(15), 1,
       sym_identifier,
-    ACTIONS(33), 1,
+    ACTIONS(17), 1,
       anon_sym_LPAREN,
-    ACTIONS(35), 1,
+    ACTIONS(19), 1,
       sym_star,
-    ACTIONS(39), 1,
+    ACTIONS(23), 1,
       anon_sym_u03bb,
-    ACTIONS(41), 1,
+    ACTIONS(25), 1,
       anon_sym_fun,
-    ACTIONS(43), 1,
+    ACTIONS(27), 1,
       anon_sym_u220f,
-    ACTIONS(45), 1,
+    ACTIONS(29), 1,
       anon_sym_forall,
-    STATE(34), 1,
+    ACTIONS(31), 1,
+      anon_sym_let,
+    STATE(43), 1,
       sym_expr,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(41), 1,
+    STATE(46), 1,
       sym_square,
-    STATE(45), 1,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(56), 1,
       sym_sort,
-    STATE(76), 1,
+    STATE(98), 1,
       sym_app_term,
-    ACTIONS(37), 2,
+    ACTIONS(21), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(31), 2,
+    STATE(41), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1810,39 +2012,39 @@ static const uint16_t ts_small_parse_table[] = {
   [1026] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
-    ACTIONS(31), 1,
+    ACTIONS(15), 1,
       sym_identifier,
-    ACTIONS(33), 1,
+    ACTIONS(17), 1,
       anon_sym_LPAREN,
-    ACTIONS(35), 1,
+    ACTIONS(19), 1,
       sym_star,
-    ACTIONS(39), 1,
+    ACTIONS(23), 1,
       anon_sym_u03bb,
-    ACTIONS(41), 1,
+    ACTIONS(25), 1,
       anon_sym_fun,
-    ACTIONS(43), 1,
+    ACTIONS(27), 1,
       anon_sym_u220f,
-    ACTIONS(45), 1,
+    ACTIONS(29), 1,
       anon_sym_forall,
-    STATE(35), 1,
+    ACTIONS(31), 1,
+      anon_sym_let,
+    STATE(42), 1,
       sym_expr,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(41), 1,
+    STATE(46), 1,
       sym_square,
-    STATE(45), 1,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(56), 1,
       sym_sort,
-    STATE(76), 1,
+    STATE(98), 1,
       sym_app_term,
-    ACTIONS(37), 2,
+    ACTIONS(21), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(31), 2,
+    STATE(41), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1850,39 +2052,39 @@ static const uint16_t ts_small_parse_table[] = {
   [1083] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
     ACTIONS(31), 1,
-      sym_identifier,
+      anon_sym_let,
     ACTIONS(33), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
       sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
     ACTIONS(41), 1,
-      anon_sym_fun,
+      anon_sym_u03bb,
     ACTIONS(43), 1,
-      anon_sym_u220f,
+      anon_sym_fun,
     ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
       anon_sym_forall,
-    STATE(38), 1,
-      sym_arrow,
-    STATE(39), 1,
-      sym_expr,
-    STATE(41), 1,
+    STATE(29), 1,
       sym_square,
-    STATE(45), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(76), 1,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(53), 1,
       sym_app_term,
-    ACTIONS(37), 2,
+    STATE(87), 1,
+      sym_expr,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(31), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1890,941 +2092,1465 @@ static const uint16_t ts_small_parse_table[] = {
   [1140] = 17,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(13), 1,
-      sym_identifier,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(21), 1,
-      anon_sym_u03bb,
-    ACTIONS(23), 1,
-      anon_sym_fun,
-    ACTIONS(25), 1,
-      anon_sym_u220f,
-    ACTIONS(27), 1,
-      anon_sym_forall,
-    ACTIONS(29), 1,
+    ACTIONS(31), 1,
       anon_sym_let,
-    STATE(25), 1,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
       sym_square,
-    STATE(28), 1,
+    STATE(33), 1,
       sym_sort,
-    STATE(38), 1,
+    STATE(49), 1,
       sym_arrow,
-    STATE(44), 1,
+    STATE(53), 1,
       sym_app_term,
-    STATE(100), 1,
+    STATE(122), 1,
       sym_expr,
-    ACTIONS(19), 2,
+    ACTIONS(39), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
+    STATE(27), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(36), 4,
+    STATE(52), 4,
       sym_labs,
       sym_pabs,
       sym_let,
       sym_app,
-  [1197] = 9,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(47), 1,
-      sym_identifier,
-    ACTIONS(50), 1,
-      anon_sym_LPAREN,
-    ACTIONS(55), 1,
-      sym_star,
-    STATE(25), 1,
-      sym_square,
-    STATE(28), 1,
-      sym_sort,
-    ACTIONS(58), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(23), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    ACTIONS(53), 8,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1234] = 9,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(15), 1,
-      anon_sym_LPAREN,
-    ACTIONS(17), 1,
-      sym_star,
-    ACTIONS(61), 1,
-      sym_identifier,
-    STATE(25), 1,
-      sym_square,
-    STATE(28), 1,
-      sym_sort,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(23), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    ACTIONS(63), 8,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1271] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(67), 1,
-      aux_sym_sort_token1,
-    ACTIONS(65), 13,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1293] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(69), 14,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      aux_sym_sort_token1,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1313] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(71), 13,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1332] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(73), 13,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1351] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(75), 13,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1370] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(65), 13,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1389] = 10,
+  [1197] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(31), 1,
-      sym_identifier,
+      anon_sym_let,
     ACTIONS(33), 1,
-      anon_sym_LPAREN,
+      sym_identifier,
     ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
       sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
+      sym_square,
+    STATE(33), 1,
+      sym_sort,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(53), 1,
+      sym_app_term,
+    STATE(123), 1,
+      sym_expr,
+    ACTIONS(39), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(27), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(52), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [1254] = 17,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(31), 1,
+      anon_sym_let,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
+      sym_square,
+    STATE(33), 1,
+      sym_sort,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(53), 1,
+      sym_app_term,
+    STATE(148), 1,
+      sym_expr,
+    ACTIONS(39), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(27), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(52), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [1311] = 17,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(31), 1,
+      anon_sym_let,
+    ACTIONS(33), 1,
+      sym_identifier,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(41), 1,
+      anon_sym_u03bb,
+    ACTIONS(43), 1,
+      anon_sym_fun,
+    ACTIONS(45), 1,
+      anon_sym_u220f,
+    ACTIONS(47), 1,
+      anon_sym_forall,
+    STATE(29), 1,
+      sym_square,
+    STATE(33), 1,
+      sym_sort,
+    STATE(49), 1,
+      sym_arrow,
+    STATE(53), 1,
+      sym_app_term,
+    STATE(129), 1,
+      sym_expr,
+    ACTIONS(39), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(27), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(52), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [1368] = 9,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(49), 1,
+      sym_identifier,
+    ACTIONS(54), 1,
+      anon_sym_LPAREN,
+    ACTIONS(57), 1,
+      sym_star,
+    STATE(29), 1,
+      sym_square,
+    STATE(33), 1,
+      sym_sort,
+    ACTIONS(60), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(26), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    ACTIONS(52), 8,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1405] = 9,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(35), 1,
+      anon_sym_LPAREN,
+    ACTIONS(37), 1,
+      sym_star,
+    ACTIONS(63), 1,
+      sym_identifier,
+    STATE(29), 1,
+      sym_square,
+    STATE(33), 1,
+      sym_sort,
+    ACTIONS(39), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(26), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    ACTIONS(65), 8,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1442] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(67), 14,
+      sym_identifier,
+      anon_sym_SEMI,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      aux_sym_sort_token1,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1462] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(71), 1,
+      aux_sym_sort_token1,
+    ACTIONS(69), 13,
+      sym_identifier,
+      anon_sym_SEMI,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1484] = 8,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(73), 1,
+      anon_sym_section,
     ACTIONS(77), 1,
-      anon_sym_end,
-    STATE(41), 1,
-      sym_square,
-    STATE(45), 1,
-      sym_sort,
-    ACTIONS(37), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    ACTIONS(63), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-    STATE(32), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-  [1423] = 10,
-    ACTIONS(3), 1,
-      sym_comment,
+      anon_sym_axiom,
     ACTIONS(79), 1,
-      sym_identifier,
-    ACTIONS(82), 1,
-      anon_sym_LPAREN,
+      anon_sym_def,
+    ACTIONS(81), 1,
+      sym_command,
+    STATE(134), 1,
+      sym_program,
+    ACTIONS(75), 2,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+    STATE(34), 6,
+      sym_section,
+      sym_variable,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1515] = 8,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(83), 1,
+      ts_builtin_sym_end,
     ACTIONS(85), 1,
-      sym_star,
+      anon_sym_section,
     ACTIONS(91), 1,
-      anon_sym_end,
-    STATE(41), 1,
-      sym_square,
-    STATE(45), 1,
-      sym_sort,
-    ACTIONS(53), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
+      anon_sym_axiom,
+    ACTIONS(94), 1,
+      anon_sym_def,
+    ACTIONS(97), 1,
+      sym_command,
     ACTIONS(88), 2,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+    STATE(31), 6,
+      sym_section,
+      sym_variable,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1546] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(100), 13,
+      sym_identifier,
+      anon_sym_SEMI,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(32), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1565] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(102), 13,
+      sym_identifier,
+      anon_sym_SEMI,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1584] = 8,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(73), 1,
+      anon_sym_section,
+    ACTIONS(77), 1,
+      anon_sym_axiom,
+    ACTIONS(79), 1,
+      anon_sym_def,
+    ACTIONS(81), 1,
+      sym_command,
+    ACTIONS(104), 1,
+      anon_sym_end,
+    ACTIONS(75), 2,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+    STATE(37), 6,
+      sym_section,
+      sym_variable,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1615] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(69), 13,
+      sym_identifier,
+      anon_sym_SEMI,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1634] = 8,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(5), 1,
+      anon_sym_section,
+    ACTIONS(9), 1,
+      anon_sym_axiom,
+    ACTIONS(11), 1,
+      anon_sym_def,
+    ACTIONS(13), 1,
+      sym_command,
+    ACTIONS(104), 1,
+      ts_builtin_sym_end,
+    ACTIONS(7), 2,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+    STATE(31), 6,
+      sym_section,
+      sym_variable,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1665] = 8,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(83), 1,
+      anon_sym_end,
+    ACTIONS(106), 1,
+      anon_sym_section,
+    ACTIONS(112), 1,
+      anon_sym_axiom,
+    ACTIONS(115), 1,
+      anon_sym_def,
+    ACTIONS(118), 1,
+      sym_command,
+    ACTIONS(109), 2,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+    STATE(37), 6,
+      sym_section,
+      sym_variable,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1696] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(121), 13,
+      sym_identifier,
+      anon_sym_SEMI,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1715] = 8,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(73), 1,
+      anon_sym_section,
+    ACTIONS(77), 1,
+      anon_sym_axiom,
+    ACTIONS(79), 1,
+      anon_sym_def,
+    ACTIONS(81), 1,
+      sym_command,
+    STATE(132), 1,
+      sym_program,
+    ACTIONS(75), 2,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+    STATE(34), 6,
+      sym_section,
+      sym_variable,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1746] = 10,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(123), 1,
+      sym_identifier,
+    ACTIONS(126), 1,
+      anon_sym_end,
+    ACTIONS(128), 1,
+      anon_sym_LPAREN,
+    ACTIONS(131), 1,
+      sym_star,
+    STATE(46), 1,
+      sym_square,
+    STATE(56), 1,
+      sym_sort,
+    ACTIONS(52), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    ACTIONS(134), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(40), 2,
       sym_term,
       aux_sym_app_repeat1,
-  [1457] = 2,
+  [1780] = 10,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(93), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1472] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(95), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1487] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(97), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1502] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(99), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1517] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(101), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1532] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(103), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1547] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(105), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1562] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(107), 2,
+    ACTIONS(15), 1,
       sym_identifier,
-      anon_sym_end,
-    ACTIONS(69), 7,
+    ACTIONS(17), 1,
       anon_sym_LPAREN,
+    ACTIONS(19), 1,
       sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      aux_sym_sort_token1,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1579] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(111), 1,
-      aux_sym_sort_token1,
-    ACTIONS(109), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(65), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1598] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(113), 9,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_SEMI,
-  [1613] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(7), 1,
-      anon_sym_axiom,
-    ACTIONS(9), 1,
-      anon_sym_def,
-    ACTIONS(11), 1,
-      sym_command,
-    ACTIONS(115), 1,
-      ts_builtin_sym_end,
-    STATE(50), 4,
-      sym_axiom,
-      sym_definition,
-      sym_preprocess,
-      aux_sym_program_repeat1,
-  [1635] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(117), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-    ACTIONS(103), 6,
-      anon_sym_RPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [1651] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(119), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(73), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1667] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(109), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(65), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1683] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(121), 1,
-      anon_sym_LPAREN,
-    ACTIONS(124), 1,
-      anon_sym_COLON,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-    ACTIONS(126), 4,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-  [1703] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(128), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(71), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1719] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(130), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(75), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1735] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(132), 1,
-      ts_builtin_sym_end,
-    ACTIONS(134), 1,
-      anon_sym_axiom,
     ACTIONS(137), 1,
-      anon_sym_def,
-    ACTIONS(140), 1,
-      sym_command,
-    STATE(50), 4,
-      sym_axiom,
-      sym_definition,
-      sym_preprocess,
-      aux_sym_program_repeat1,
-  [1757] = 6,
+      anon_sym_end,
+    STATE(46), 1,
+      sym_square,
+    STATE(56), 1,
+      sym_sort,
+    ACTIONS(21), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    ACTIONS(65), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    STATE(40), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+  [1814] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(145), 1,
-      anon_sym_COLON,
-    STATE(83), 1,
-      sym_ascription,
-    ACTIONS(147), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1778] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(145), 1,
-      anon_sym_COLON,
-    STATE(84), 1,
-      sym_ascription,
-    ACTIONS(149), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1799] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(151), 1,
-      anon_sym_COLON,
-    ACTIONS(153), 1,
-      anon_sym_COLON_EQ,
-    STATE(87), 1,
-      sym_ascription,
-    STATE(56), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1819] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(157), 1,
-      anon_sym_COLON,
-    ACTIONS(155), 5,
-      anon_sym_LPAREN,
+    ACTIONS(139), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
       anon_sym_COMMA,
       anon_sym_COLON_EQ,
-  [1833] = 6,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1829] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(151), 1,
-      anon_sym_COLON,
-    ACTIONS(159), 1,
-      anon_sym_COLON_EQ,
-    STATE(102), 1,
-      sym_ascription,
-    STATE(57), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1853] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(151), 1,
-      anon_sym_COLON,
-    ACTIONS(161), 1,
-      anon_sym_COLON_EQ,
-    STATE(89), 1,
-      sym_ascription,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1873] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(151), 1,
-      anon_sym_COLON,
-    ACTIONS(163), 1,
-      anon_sym_COLON_EQ,
-    STATE(95), 1,
-      sym_ascription,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1893] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(145), 1,
-      anon_sym_COLON,
-    ACTIONS(165), 1,
+    ACTIONS(141), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
       anon_sym_COMMA,
-    STATE(97), 1,
-      sym_ascription,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1913] = 6,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1844] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(145), 1,
-      anon_sym_COLON,
-    ACTIONS(167), 1,
+    ACTIONS(143), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
       anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1859] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(147), 1,
+      anon_sym_LPAREN,
+    ACTIONS(150), 1,
+      anon_sym_COLON,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+    ACTIONS(145), 5,
+      anon_sym_SEMI,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+  [1880] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(154), 1,
+      aux_sym_sort_token1,
+    ACTIONS(152), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(69), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1899] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(156), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1914] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(158), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(67), 7,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      aux_sym_sort_token1,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1931] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(160), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1946] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(162), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1961] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(164), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1976] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(166), 9,
+      anon_sym_end,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1991] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(168), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    ACTIONS(160), 6,
+      anon_sym_SEMI,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+  [2007] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(170), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(100), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [2023] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(172), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(121), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [2039] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(174), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(102), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [2055] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(152), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(69), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [2071] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
     STATE(104), 1,
       sym_ascription,
-    STATE(47), 2,
+    ACTIONS(180), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+    STATE(45), 2,
       sym_param_block,
-      aux_sym_labs_repeat1,
-  [1933] = 5,
+      aux_sym_variable_repeat1,
+  [2092] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    ACTIONS(145), 1,
+    ACTIONS(182), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2105] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(184), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2118] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(182), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2131] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(186), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2144] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(190), 1,
       anon_sym_COLON,
-    STATE(88), 1,
-      sym_ascription,
-    STATE(61), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1950] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
+    ACTIONS(188), 6,
+      anon_sym_SEMI,
       anon_sym_LPAREN,
-    ACTIONS(145), 1,
-      anon_sym_COLON,
-    STATE(105), 1,
-      sym_ascription,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1967] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(169), 5,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
       anon_sym_COMMA,
       anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [1978] = 2,
+  [2159] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(171), 4,
+    ACTIONS(192), 7,
       ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
       anon_sym_axiom,
       anon_sym_def,
       sym_command,
-  [1988] = 4,
+  [2172] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(173), 1,
-      anon_sym_LPAREN,
-    ACTIONS(175), 1,
-      anon_sym_in,
-    STATE(68), 2,
-      sym_binding,
-      aux_sym_let_repeat1,
-  [2002] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(177), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [2012] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(179), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [2022] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(181), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [2032] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(183), 1,
-      anon_sym_LPAREN,
-    ACTIONS(186), 1,
-      anon_sym_in,
-    STATE(68), 2,
-      sym_binding,
-      aux_sym_let_repeat1,
-  [2046] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(188), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [2056] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(190), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [2066] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(192), 1,
-      sym_identifier,
-    ACTIONS(195), 1,
-      anon_sym_COLON,
-    STATE(71), 1,
-      aux_sym_param_block_repeat1,
-  [2079] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    STATE(51), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [2090] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    STATE(58), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [2101] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(173), 1,
-      anon_sym_LPAREN,
-    STATE(64), 2,
-      sym_binding,
-      aux_sym_let_repeat1,
-  [2112] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(197), 1,
-      sym_identifier,
-    ACTIONS(199), 1,
-      anon_sym_COLON,
-    STATE(71), 1,
-      aux_sym_param_block_repeat1,
-  [2125] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(103), 1,
+    ACTIONS(194), 7,
+      anon_sym_section,
       anon_sym_end,
-    ACTIONS(201), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [2136] = 3,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2185] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(143), 1,
+    ACTIONS(196), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2198] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(196), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2211] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(186), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2224] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(198), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2237] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
       anon_sym_LPAREN,
-    STATE(52), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [2147] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(143), 1,
-      anon_sym_LPAREN,
-    STATE(59), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [2158] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(203), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [2166] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(205), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [2174] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(207), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [2182] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(209), 1,
-      sym_identifier,
-    STATE(75), 1,
-      aux_sym_param_block_repeat1,
-  [2192] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(211), 2,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    STATE(109), 1,
+      sym_ascription,
+    ACTIONS(200), 2,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
-  [2200] = 2,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2258] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(213), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-  [2208] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(215), 1,
-      anon_sym_RPAREN,
-  [2215] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(217), 1,
-      anon_sym_SEMI,
-  [2222] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(161), 1,
-      anon_sym_COLON_EQ,
-  [2229] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(219), 1,
-      anon_sym_SEMI,
-  [2236] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(221), 1,
-      anon_sym_COLON_EQ,
-  [2243] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(223), 1,
-      anon_sym_SEMI,
-  [2250] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(225), 1,
-      sym_identifier,
-  [2257] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(227), 1,
-      anon_sym_RPAREN,
-  [2264] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(229), 1,
-      anon_sym_RPAREN,
+    ACTIONS(202), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
   [2271] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(231), 1,
-      sym_identifier,
-  [2278] = 2,
+    ACTIONS(192), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2284] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(233), 1,
+    ACTIONS(194), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2297] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(184), 7,
+      anon_sym_section,
+      anon_sym_end,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2310] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(198), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2323] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(202), 7,
+      ts_builtin_sym_end,
+      anon_sym_section,
+      anon_sym_variable,
+      anon_sym_hypothesis,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [2336] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    ACTIONS(204), 1,
+      anon_sym_COMMA,
+    STATE(128), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2356] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(206), 1,
+      anon_sym_COLON,
+    ACTIONS(208), 1,
       anon_sym_COLON_EQ,
-  [2285] = 2,
+    STATE(126), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2376] = 6,
     ACTIONS(3), 1,
       sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(206), 1,
+      anon_sym_COLON,
+    ACTIONS(210), 1,
+      anon_sym_COLON_EQ,
+    STATE(136), 1,
+      sym_ascription,
+    STATE(80), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2396] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(206), 1,
+      anon_sym_COLON,
+    ACTIONS(212), 1,
+      anon_sym_COLON_EQ,
+    STATE(113), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2416] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    ACTIONS(214), 1,
+      anon_sym_COMMA,
+    STATE(111), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2436] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(206), 1,
+      anon_sym_COLON,
+    ACTIONS(216), 1,
+      anon_sym_COLON_EQ,
+    STATE(127), 1,
+      sym_ascription,
+    STATE(78), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2456] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(206), 1,
+      anon_sym_COLON,
+    ACTIONS(218), 1,
+      anon_sym_COLON_EQ,
+    STATE(145), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2476] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(206), 1,
+      anon_sym_COLON,
+    ACTIONS(220), 1,
+      anon_sym_COLON_EQ,
+    STATE(143), 1,
+      sym_ascription,
+    STATE(83), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2496] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    STATE(131), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2513] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    STATE(144), 1,
+      sym_ascription,
+    STATE(85), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2530] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(222), 5,
+      anon_sym_SEMI,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+  [2541] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    STATE(121), 1,
+      sym_ascription,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2558] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(178), 1,
+      anon_sym_COLON,
+    STATE(118), 1,
+      sym_ascription,
+    STATE(88), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2575] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(224), 1,
+      anon_sym_SEMI,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2589] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(226), 1,
+      anon_sym_LPAREN,
+    ACTIONS(228), 1,
+      anon_sym_in,
+    STATE(93), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [2603] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    ACTIONS(230), 1,
+      anon_sym_SEMI,
+    STATE(45), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2617] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(232), 1,
+      anon_sym_LPAREN,
     ACTIONS(235), 1,
-      sym_identifier,
-  [2292] = 2,
+      anon_sym_in,
+    STATE(93), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [2631] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    STATE(90), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2642] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    STATE(58), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2653] = 4,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(237), 1,
-      anon_sym_COMMA,
-  [2299] = 2,
+      sym_identifier,
+    ACTIONS(240), 1,
+      anon_sym_COLON,
+    STATE(96), 1,
+      aux_sym_param_block_repeat1,
+  [2666] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(239), 1,
-      anon_sym_SEMI,
-  [2306] = 2,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    STATE(81), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2677] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(241), 1,
-      ts_builtin_sym_end,
-  [2313] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(243), 1,
-      anon_sym_RPAREN,
-  [2320] = 2,
-    ACTIONS(245), 1,
-      sym_comment,
-    ACTIONS(247), 1,
-      sym_post_command,
-  [2327] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(163), 1,
-      anon_sym_COLON_EQ,
-  [2334] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(249), 1,
-      anon_sym_RPAREN,
-  [2341] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(251), 1,
-      anon_sym_COMMA,
-  [2348] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(253), 1,
-      anon_sym_SEMI,
-  [2355] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(255), 1,
-      anon_sym_RPAREN,
-  [2362] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(257), 1,
+    ACTIONS(160), 1,
       anon_sym_end,
+    ACTIONS(242), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [2688] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(244), 1,
+      sym_identifier,
+    ACTIONS(246), 1,
+      anon_sym_COLON,
+    STATE(96), 1,
+      aux_sym_param_block_repeat1,
+  [2701] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    STATE(77), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2712] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(226), 1,
+      anon_sym_LPAREN,
+    STATE(91), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [2723] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    STATE(70), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2734] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(176), 1,
+      anon_sym_LPAREN,
+    STATE(92), 2,
+      sym_param_block,
+      aux_sym_variable_repeat1,
+  [2745] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(248), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+  [2753] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(250), 1,
+      sym_identifier,
+    STATE(99), 1,
+      aux_sym_param_block_repeat1,
+  [2763] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(252), 2,
+      anon_sym_LPAREN,
+      anon_sym_in,
+  [2771] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(254), 2,
+      anon_sym_LPAREN,
+      anon_sym_in,
+  [2779] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(256), 2,
+      anon_sym_LPAREN,
+      anon_sym_in,
+  [2787] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(258), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+  [2795] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(260), 1,
+      sym_identifier,
+  [2802] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(262), 1,
+      anon_sym_COMMA,
+  [2809] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(264), 1,
+      anon_sym_end,
+  [2816] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(266), 1,
+      anon_sym_COLON_EQ,
+  [2823] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(268), 1,
+      anon_sym_RPAREN,
+  [2830] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(270), 1,
+      sym_identifier,
+  [2837] = 2,
+    ACTIONS(272), 1,
+      sym_comment,
+    ACTIONS(274), 1,
+      sym_post_command,
+  [2844] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(276), 1,
+      anon_sym_RPAREN,
+  [2851] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(278), 1,
+      anon_sym_SEMI,
+  [2858] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(280), 1,
+      sym_identifier,
+  [2865] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(282), 1,
+      anon_sym_RPAREN,
+  [2872] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(284), 1,
+      anon_sym_SEMI,
+  [2879] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(286), 1,
+      anon_sym_SEMI,
+  [2886] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(288), 1,
+      anon_sym_RPAREN,
+  [2893] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(290), 1,
+      anon_sym_SEMI,
+  [2900] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(292), 1,
+      anon_sym_SEMI,
+  [2907] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(294), 1,
+      anon_sym_COLON_EQ,
+  [2914] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(208), 1,
+      anon_sym_COLON_EQ,
+  [2921] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(296), 1,
+      anon_sym_COMMA,
+  [2928] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(298), 1,
+      anon_sym_SEMI,
+  [2935] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(300), 1,
+      sym_identifier,
+  [2942] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(302), 1,
+      anon_sym_SEMI,
+  [2949] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(304), 1,
+      anon_sym_end,
+  [2956] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(306), 1,
+      sym_identifier,
+  [2963] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(308), 1,
+      anon_sym_end,
+  [2970] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(310), 1,
+      anon_sym_SEMI,
+  [2977] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(212), 1,
+      anon_sym_COLON_EQ,
+  [2984] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(312), 1,
+      anon_sym_RPAREN,
+  [2991] = 2,
+    ACTIONS(272), 1,
+      sym_comment,
+    ACTIONS(314), 1,
+      sym_post_command,
+  [2998] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(316), 1,
+      sym_identifier,
+  [3005] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(318), 1,
+      sym_identifier,
+  [3012] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(320), 1,
+      ts_builtin_sym_end,
+  [3019] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(322), 1,
+      anon_sym_RPAREN,
+  [3026] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(218), 1,
+      anon_sym_COLON_EQ,
+  [3033] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(324), 1,
+      anon_sym_SEMI,
+  [3040] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(326), 1,
+      anon_sym_COLON_EQ,
+  [3047] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(328), 1,
+      sym_identifier,
+  [3054] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(330), 1,
+      sym_identifier,
+  [3061] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(332), 1,
+      anon_sym_SEMI,
 };
 
 static const uint32_t ts_small_parse_table_map[] = {
@@ -2850,216 +3576,291 @@ static const uint32_t ts_small_parse_table_map[] = {
   [SMALL_STATE(21)] = 1083,
   [SMALL_STATE(22)] = 1140,
   [SMALL_STATE(23)] = 1197,
-  [SMALL_STATE(24)] = 1234,
-  [SMALL_STATE(25)] = 1271,
-  [SMALL_STATE(26)] = 1293,
-  [SMALL_STATE(27)] = 1313,
-  [SMALL_STATE(28)] = 1332,
-  [SMALL_STATE(29)] = 1351,
-  [SMALL_STATE(30)] = 1370,
-  [SMALL_STATE(31)] = 1389,
-  [SMALL_STATE(32)] = 1423,
-  [SMALL_STATE(33)] = 1457,
-  [SMALL_STATE(34)] = 1472,
-  [SMALL_STATE(35)] = 1487,
-  [SMALL_STATE(36)] = 1502,
-  [SMALL_STATE(37)] = 1517,
-  [SMALL_STATE(38)] = 1532,
-  [SMALL_STATE(39)] = 1547,
-  [SMALL_STATE(40)] = 1562,
-  [SMALL_STATE(41)] = 1579,
-  [SMALL_STATE(42)] = 1598,
-  [SMALL_STATE(43)] = 1613,
-  [SMALL_STATE(44)] = 1635,
-  [SMALL_STATE(45)] = 1651,
-  [SMALL_STATE(46)] = 1667,
-  [SMALL_STATE(47)] = 1683,
-  [SMALL_STATE(48)] = 1703,
-  [SMALL_STATE(49)] = 1719,
-  [SMALL_STATE(50)] = 1735,
-  [SMALL_STATE(51)] = 1757,
-  [SMALL_STATE(52)] = 1778,
-  [SMALL_STATE(53)] = 1799,
-  [SMALL_STATE(54)] = 1819,
-  [SMALL_STATE(55)] = 1833,
-  [SMALL_STATE(56)] = 1853,
-  [SMALL_STATE(57)] = 1873,
-  [SMALL_STATE(58)] = 1893,
-  [SMALL_STATE(59)] = 1913,
-  [SMALL_STATE(60)] = 1933,
-  [SMALL_STATE(61)] = 1950,
-  [SMALL_STATE(62)] = 1967,
-  [SMALL_STATE(63)] = 1978,
-  [SMALL_STATE(64)] = 1988,
-  [SMALL_STATE(65)] = 2002,
-  [SMALL_STATE(66)] = 2012,
-  [SMALL_STATE(67)] = 2022,
-  [SMALL_STATE(68)] = 2032,
-  [SMALL_STATE(69)] = 2046,
-  [SMALL_STATE(70)] = 2056,
-  [SMALL_STATE(71)] = 2066,
-  [SMALL_STATE(72)] = 2079,
-  [SMALL_STATE(73)] = 2090,
-  [SMALL_STATE(74)] = 2101,
-  [SMALL_STATE(75)] = 2112,
-  [SMALL_STATE(76)] = 2125,
-  [SMALL_STATE(77)] = 2136,
-  [SMALL_STATE(78)] = 2147,
-  [SMALL_STATE(79)] = 2158,
-  [SMALL_STATE(80)] = 2166,
-  [SMALL_STATE(81)] = 2174,
-  [SMALL_STATE(82)] = 2182,
-  [SMALL_STATE(83)] = 2192,
-  [SMALL_STATE(84)] = 2200,
-  [SMALL_STATE(85)] = 2208,
-  [SMALL_STATE(86)] = 2215,
-  [SMALL_STATE(87)] = 2222,
-  [SMALL_STATE(88)] = 2229,
-  [SMALL_STATE(89)] = 2236,
-  [SMALL_STATE(90)] = 2243,
-  [SMALL_STATE(91)] = 2250,
-  [SMALL_STATE(92)] = 2257,
-  [SMALL_STATE(93)] = 2264,
-  [SMALL_STATE(94)] = 2271,
-  [SMALL_STATE(95)] = 2278,
-  [SMALL_STATE(96)] = 2285,
-  [SMALL_STATE(97)] = 2292,
-  [SMALL_STATE(98)] = 2299,
-  [SMALL_STATE(99)] = 2306,
-  [SMALL_STATE(100)] = 2313,
-  [SMALL_STATE(101)] = 2320,
-  [SMALL_STATE(102)] = 2327,
-  [SMALL_STATE(103)] = 2334,
-  [SMALL_STATE(104)] = 2341,
-  [SMALL_STATE(105)] = 2348,
-  [SMALL_STATE(106)] = 2355,
-  [SMALL_STATE(107)] = 2362,
+  [SMALL_STATE(24)] = 1254,
+  [SMALL_STATE(25)] = 1311,
+  [SMALL_STATE(26)] = 1368,
+  [SMALL_STATE(27)] = 1405,
+  [SMALL_STATE(28)] = 1442,
+  [SMALL_STATE(29)] = 1462,
+  [SMALL_STATE(30)] = 1484,
+  [SMALL_STATE(31)] = 1515,
+  [SMALL_STATE(32)] = 1546,
+  [SMALL_STATE(33)] = 1565,
+  [SMALL_STATE(34)] = 1584,
+  [SMALL_STATE(35)] = 1615,
+  [SMALL_STATE(36)] = 1634,
+  [SMALL_STATE(37)] = 1665,
+  [SMALL_STATE(38)] = 1696,
+  [SMALL_STATE(39)] = 1715,
+  [SMALL_STATE(40)] = 1746,
+  [SMALL_STATE(41)] = 1780,
+  [SMALL_STATE(42)] = 1814,
+  [SMALL_STATE(43)] = 1829,
+  [SMALL_STATE(44)] = 1844,
+  [SMALL_STATE(45)] = 1859,
+  [SMALL_STATE(46)] = 1880,
+  [SMALL_STATE(47)] = 1899,
+  [SMALL_STATE(48)] = 1914,
+  [SMALL_STATE(49)] = 1931,
+  [SMALL_STATE(50)] = 1946,
+  [SMALL_STATE(51)] = 1961,
+  [SMALL_STATE(52)] = 1976,
+  [SMALL_STATE(53)] = 1991,
+  [SMALL_STATE(54)] = 2007,
+  [SMALL_STATE(55)] = 2023,
+  [SMALL_STATE(56)] = 2039,
+  [SMALL_STATE(57)] = 2055,
+  [SMALL_STATE(58)] = 2071,
+  [SMALL_STATE(59)] = 2092,
+  [SMALL_STATE(60)] = 2105,
+  [SMALL_STATE(61)] = 2118,
+  [SMALL_STATE(62)] = 2131,
+  [SMALL_STATE(63)] = 2144,
+  [SMALL_STATE(64)] = 2159,
+  [SMALL_STATE(65)] = 2172,
+  [SMALL_STATE(66)] = 2185,
+  [SMALL_STATE(67)] = 2198,
+  [SMALL_STATE(68)] = 2211,
+  [SMALL_STATE(69)] = 2224,
+  [SMALL_STATE(70)] = 2237,
+  [SMALL_STATE(71)] = 2258,
+  [SMALL_STATE(72)] = 2271,
+  [SMALL_STATE(73)] = 2284,
+  [SMALL_STATE(74)] = 2297,
+  [SMALL_STATE(75)] = 2310,
+  [SMALL_STATE(76)] = 2323,
+  [SMALL_STATE(77)] = 2336,
+  [SMALL_STATE(78)] = 2356,
+  [SMALL_STATE(79)] = 2376,
+  [SMALL_STATE(80)] = 2396,
+  [SMALL_STATE(81)] = 2416,
+  [SMALL_STATE(82)] = 2436,
+  [SMALL_STATE(83)] = 2456,
+  [SMALL_STATE(84)] = 2476,
+  [SMALL_STATE(85)] = 2496,
+  [SMALL_STATE(86)] = 2513,
+  [SMALL_STATE(87)] = 2530,
+  [SMALL_STATE(88)] = 2541,
+  [SMALL_STATE(89)] = 2558,
+  [SMALL_STATE(90)] = 2575,
+  [SMALL_STATE(91)] = 2589,
+  [SMALL_STATE(92)] = 2603,
+  [SMALL_STATE(93)] = 2617,
+  [SMALL_STATE(94)] = 2631,
+  [SMALL_STATE(95)] = 2642,
+  [SMALL_STATE(96)] = 2653,
+  [SMALL_STATE(97)] = 2666,
+  [SMALL_STATE(98)] = 2677,
+  [SMALL_STATE(99)] = 2688,
+  [SMALL_STATE(100)] = 2701,
+  [SMALL_STATE(101)] = 2712,
+  [SMALL_STATE(102)] = 2723,
+  [SMALL_STATE(103)] = 2734,
+  [SMALL_STATE(104)] = 2745,
+  [SMALL_STATE(105)] = 2753,
+  [SMALL_STATE(106)] = 2763,
+  [SMALL_STATE(107)] = 2771,
+  [SMALL_STATE(108)] = 2779,
+  [SMALL_STATE(109)] = 2787,
+  [SMALL_STATE(110)] = 2795,
+  [SMALL_STATE(111)] = 2802,
+  [SMALL_STATE(112)] = 2809,
+  [SMALL_STATE(113)] = 2816,
+  [SMALL_STATE(114)] = 2823,
+  [SMALL_STATE(115)] = 2830,
+  [SMALL_STATE(116)] = 2837,
+  [SMALL_STATE(117)] = 2844,
+  [SMALL_STATE(118)] = 2851,
+  [SMALL_STATE(119)] = 2858,
+  [SMALL_STATE(120)] = 2865,
+  [SMALL_STATE(121)] = 2872,
+  [SMALL_STATE(122)] = 2879,
+  [SMALL_STATE(123)] = 2886,
+  [SMALL_STATE(124)] = 2893,
+  [SMALL_STATE(125)] = 2900,
+  [SMALL_STATE(126)] = 2907,
+  [SMALL_STATE(127)] = 2914,
+  [SMALL_STATE(128)] = 2921,
+  [SMALL_STATE(129)] = 2928,
+  [SMALL_STATE(130)] = 2935,
+  [SMALL_STATE(131)] = 2942,
+  [SMALL_STATE(132)] = 2949,
+  [SMALL_STATE(133)] = 2956,
+  [SMALL_STATE(134)] = 2963,
+  [SMALL_STATE(135)] = 2970,
+  [SMALL_STATE(136)] = 2977,
+  [SMALL_STATE(137)] = 2984,
+  [SMALL_STATE(138)] = 2991,
+  [SMALL_STATE(139)] = 2998,
+  [SMALL_STATE(140)] = 3005,
+  [SMALL_STATE(141)] = 3012,
+  [SMALL_STATE(142)] = 3019,
+  [SMALL_STATE(143)] = 3026,
+  [SMALL_STATE(144)] = 3033,
+  [SMALL_STATE(145)] = 3040,
+  [SMALL_STATE(146)] = 3047,
+  [SMALL_STATE(147)] = 3054,
+  [SMALL_STATE(148)] = 3061,
 };
 
 static const TSParseActionEntry ts_parse_actions[] = {
   [0] = {.entry = {.count = 0, .reusable = false}},
   [1] = {.entry = {.count = 1, .reusable = false}}, RECOVER(),
   [3] = {.entry = {.count = 1, .reusable = true}}, SHIFT_EXTRA(),
-  [5] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 0, 0, 0),
-  [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(96),
-  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(91),
-  [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(101),
-  [13] = {.entry = {.count = 1, .reusable = false}}, SHIFT(28),
-  [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6),
-  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(30),
-  [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(26),
-  [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(72),
-  [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(72),
-  [25] = {.entry = {.count = 1, .reusable = true}}, SHIFT(73),
-  [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(73),
-  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(74),
-  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(45),
-  [33] = {.entry = {.count = 1, .reusable = true}}, SHIFT(22),
-  [35] = {.entry = {.count = 1, .reusable = true}}, SHIFT(46),
-  [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(40),
-  [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(77),
-  [41] = {.entry = {.count = 1, .reusable = false}}, SHIFT(77),
-  [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(78),
-  [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(78),
-  [47] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(28),
-  [50] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(6),
-  [53] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
-  [55] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(30),
-  [58] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(26),
-  [61] = {.entry = {.count = 1, .reusable = true}}, SHIFT(28),
-  [63] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
-  [65] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_sort, 1, 0, 0),
-  [67] = {.entry = {.count = 1, .reusable = true}}, SHIFT(27),
-  [69] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
-  [71] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_sort, 2, 0, 0),
-  [73] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
-  [75] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
-  [77] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0),
-  [79] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(45),
-  [82] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(22),
-  [85] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(46),
-  [88] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(40),
-  [91] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
-  [93] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
-  [95] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
-  [97] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
-  [99] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
-  [101] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 5, 0, 0),
-  [103] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
-  [105] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 5, 0, 0),
-  [107] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0),
-  [109] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_sort, 1, 0, 0),
-  [111] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48),
-  [113] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0),
-  [115] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
-  [117] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
-  [119] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0),
-  [121] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(82),
-  [124] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [126] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [128] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_sort, 2, 0, 0),
-  [130] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0),
-  [132] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
-  [134] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(96),
-  [137] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(91),
-  [140] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(101),
-  [143] = {.entry = {.count = 1, .reusable = true}}, SHIFT(82),
-  [145] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4),
-  [147] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
-  [149] = {.entry = {.count = 1, .reusable = true}}, SHIFT(19),
-  [151] = {.entry = {.count = 1, .reusable = false}}, SHIFT(4),
-  [153] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5),
-  [155] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3),
-  [157] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3),
-  [159] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
-  [161] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
-  [163] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
-  [165] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
-  [167] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20),
-  [169] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
-  [171] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
-  [173] = {.entry = {.count = 1, .reusable = true}}, SHIFT(94),
-  [175] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12),
-  [177] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 7, 0, 2),
-  [179] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
-  [181] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
-  [183] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(94),
-  [186] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0),
-  [188] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 5, 0, 2),
-  [190] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 4, 0, 2),
-  [192] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(71),
-  [195] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
-  [197] = {.entry = {.count = 1, .reusable = true}}, SHIFT(71),
-  [199] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
-  [201] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18),
-  [203] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0),
-  [205] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0),
-  [207] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 7, 0, 0),
-  [209] = {.entry = {.count = 1, .reusable = true}}, SHIFT(75),
-  [211] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13),
-  [213] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21),
-  [215] = {.entry = {.count = 1, .reusable = true}}, SHIFT(80),
-  [217] = {.entry = {.count = 1, .reusable = true}}, SHIFT(67),
-  [219] = {.entry = {.count = 1, .reusable = true}}, SHIFT(70),
-  [221] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
-  [223] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63),
-  [225] = {.entry = {.count = 1, .reusable = true}}, SHIFT(53),
-  [227] = {.entry = {.count = 1, .reusable = true}}, SHIFT(54),
-  [229] = {.entry = {.count = 1, .reusable = true}}, SHIFT(79),
-  [231] = {.entry = {.count = 1, .reusable = true}}, SHIFT(55),
-  [233] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17),
-  [235] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60),
-  [237] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
-  [239] = {.entry = {.count = 1, .reusable = true}}, SHIFT(65),
-  [241] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
-  [243] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49),
-  [245] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
-  [247] = {.entry = {.count = 1, .reusable = false}}, SHIFT(66),
-  [249] = {.entry = {.count = 1, .reusable = true}}, SHIFT(29),
-  [251] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
-  [253] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69),
-  [255] = {.entry = {.count = 1, .reusable = true}}, SHIFT(81),
-  [257] = {.entry = {.count = 1, .reusable = true}}, SHIFT(42),
+  [5] = {.entry = {.count = 1, .reusable = true}}, SHIFT(130),
+  [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(94),
+  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(115),
+  [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(110),
+  [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(138),
+  [15] = {.entry = {.count = 1, .reusable = false}}, SHIFT(56),
+  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(23),
+  [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(57),
+  [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48),
+  [23] = {.entry = {.count = 1, .reusable = true}}, SHIFT(102),
+  [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(102),
+  [27] = {.entry = {.count = 1, .reusable = true}}, SHIFT(100),
+  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(100),
+  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(101),
+  [33] = {.entry = {.count = 1, .reusable = false}}, SHIFT(33),
+  [35] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5),
+  [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35),
+  [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(28),
+  [41] = {.entry = {.count = 1, .reusable = true}}, SHIFT(95),
+  [43] = {.entry = {.count = 1, .reusable = false}}, SHIFT(95),
+  [45] = {.entry = {.count = 1, .reusable = true}}, SHIFT(97),
+  [47] = {.entry = {.count = 1, .reusable = false}}, SHIFT(97),
+  [49] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(33),
+  [52] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
+  [54] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(5),
+  [57] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(35),
+  [60] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(28),
+  [63] = {.entry = {.count = 1, .reusable = true}}, SHIFT(33),
+  [65] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
+  [67] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
+  [69] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_sort, 1, 0, 0),
+  [71] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38),
+  [73] = {.entry = {.count = 1, .reusable = true}}, SHIFT(146),
+  [75] = {.entry = {.count = 1, .reusable = true}}, SHIFT(103),
+  [77] = {.entry = {.count = 1, .reusable = true}}, SHIFT(140),
+  [79] = {.entry = {.count = 1, .reusable = true}}, SHIFT(147),
+  [81] = {.entry = {.count = 1, .reusable = true}}, SHIFT(116),
+  [83] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
+  [85] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(130),
+  [88] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(94),
+  [91] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(115),
+  [94] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(110),
+  [97] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(138),
+  [100] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
+  [102] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
+  [104] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
+  [106] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(146),
+  [109] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(103),
+  [112] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(140),
+  [115] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(147),
+  [118] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(116),
+  [121] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_sort, 2, 0, 0),
+  [123] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(56),
+  [126] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
+  [128] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(23),
+  [131] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(57),
+  [134] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(48),
+  [137] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0),
+  [139] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 5, 0, 0),
+  [141] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 5, 0, 0),
+  [143] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0),
+  [145] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_variable_repeat1, 2, 0, 0),
+  [147] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_variable_repeat1, 2, 0, 0), SHIFT_REPEAT(105),
+  [150] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_variable_repeat1, 2, 0, 0),
+  [152] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_sort, 1, 0, 0),
+  [154] = {.entry = {.count = 1, .reusable = true}}, SHIFT(55),
+  [156] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
+  [158] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0),
+  [160] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
+  [162] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
+  [164] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
+  [166] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
+  [168] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6),
+  [170] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0),
+  [172] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_sort, 2, 0, 0),
+  [174] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0),
+  [176] = {.entry = {.count = 1, .reusable = true}}, SHIFT(105),
+  [178] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21),
+  [180] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
+  [182] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 5, 0, 2),
+  [184] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
+  [186] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
+  [188] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3),
+  [190] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3),
+  [192] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_section, 5, 0, 0),
+  [194] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_variable, 3, 0, 0),
+  [196] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
+  [198] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 7, 0, 2),
+  [200] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17),
+  [202] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 4, 0, 2),
+  [204] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18),
+  [206] = {.entry = {.count = 1, .reusable = false}}, SHIFT(21),
+  [208] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
+  [210] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
+  [212] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
+  [214] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
+  [216] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13),
+  [218] = {.entry = {.count = 1, .reusable = true}}, SHIFT(24),
+  [220] = {.entry = {.count = 1, .reusable = true}}, SHIFT(22),
+  [222] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
+  [224] = {.entry = {.count = 1, .reusable = true}}, SHIFT(73),
+  [226] = {.entry = {.count = 1, .reusable = true}}, SHIFT(133),
+  [228] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
+  [230] = {.entry = {.count = 1, .reusable = true}}, SHIFT(65),
+  [232] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(133),
+  [235] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0),
+  [237] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(96),
+  [240] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
+  [242] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
+  [244] = {.entry = {.count = 1, .reusable = true}}, SHIFT(96),
+  [246] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4),
+  [248] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
+  [250] = {.entry = {.count = 1, .reusable = true}}, SHIFT(99),
+  [252] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0),
+  [254] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0),
+  [256] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 7, 0, 0),
+  [258] = {.entry = {.count = 1, .reusable = true}}, SHIFT(19),
+  [260] = {.entry = {.count = 1, .reusable = true}}, SHIFT(79),
+  [262] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12),
+  [264] = {.entry = {.count = 1, .reusable = true}}, SHIFT(44),
+  [266] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
+  [268] = {.entry = {.count = 1, .reusable = true}}, SHIFT(108),
+  [270] = {.entry = {.count = 1, .reusable = true}}, SHIFT(86),
+  [272] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
+  [274] = {.entry = {.count = 1, .reusable = false}}, SHIFT(74),
+  [276] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63),
+  [278] = {.entry = {.count = 1, .reusable = true}}, SHIFT(71),
+  [280] = {.entry = {.count = 1, .reusable = true}}, SHIFT(72),
+  [282] = {.entry = {.count = 1, .reusable = true}}, SHIFT(32),
+  [284] = {.entry = {.count = 1, .reusable = true}}, SHIFT(61),
+  [286] = {.entry = {.count = 1, .reusable = true}}, SHIFT(62),
+  [288] = {.entry = {.count = 1, .reusable = true}}, SHIFT(54),
+  [290] = {.entry = {.count = 1, .reusable = true}}, SHIFT(67),
+  [292] = {.entry = {.count = 1, .reusable = true}}, SHIFT(75),
+  [294] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
+  [296] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20),
+  [298] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69),
+  [300] = {.entry = {.count = 1, .reusable = true}}, SHIFT(30),
+  [302] = {.entry = {.count = 1, .reusable = true}}, SHIFT(59),
+  [304] = {.entry = {.count = 1, .reusable = true}}, SHIFT(119),
+  [306] = {.entry = {.count = 1, .reusable = true}}, SHIFT(82),
+  [308] = {.entry = {.count = 1, .reusable = true}}, SHIFT(139),
+  [310] = {.entry = {.count = 1, .reusable = true}}, SHIFT(68),
+  [312] = {.entry = {.count = 1, .reusable = true}}, SHIFT(106),
+  [314] = {.entry = {.count = 1, .reusable = false}}, SHIFT(60),
+  [316] = {.entry = {.count = 1, .reusable = true}}, SHIFT(64),
+  [318] = {.entry = {.count = 1, .reusable = true}}, SHIFT(89),
+  [320] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
+  [322] = {.entry = {.count = 1, .reusable = true}}, SHIFT(107),
+  [324] = {.entry = {.count = 1, .reusable = true}}, SHIFT(76),
+  [326] = {.entry = {.count = 1, .reusable = true}}, SHIFT(25),
+  [328] = {.entry = {.count = 1, .reusable = true}}, SHIFT(39),
+  [330] = {.entry = {.count = 1, .reusable = true}}, SHIFT(84),
+  [332] = {.entry = {.count = 1, .reusable = true}}, SHIFT(66),
 };
 
 #ifdef __cplusplus
diff --git a/test/corpus/section.txt b/test/corpus/section.txt
new file mode 100644
index 0000000..023fa75
--- /dev/null
+++ b/test/corpus/section.txt
@@ -0,0 +1,72 @@
+========
+Sections
+========
+
+section Test
+    variable (A B C : *);
+    hypothesis (x : A) (y : B) (z1 z2 : C);
+
+    section Nested
+        def foo (x : A) := y;
+    end Nested
+end Test
+
+----
+
+(program
+  (section
+    (identifier)
+    (program
+      (variable
+        (param_block
+          (identifier)
+          (identifier)
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (sort
+                    (star))))))))
+      (variable
+        (param_block
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier))))))
+        (param_block
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier))))))
+        (param_block
+          (identifier)
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier)))))))
+      (section
+        (identifier)
+        (program
+          (definition
+            (identifier)
+            (param_block
+              (identifier)
+              (expr
+                (app_term
+                  (app
+                    (term
+                      (identifier))))))
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier)))))))
+        (identifier)))
+    (identifier)))