diff --git a/grammar.js b/grammar.js
index 6ee2df9..e3b4863 100644
--- a/grammar.js
+++ b/grammar.js
@@ -33,6 +33,7 @@ module.exports = grammar({
 
     star   : $ => "*",
     square : $ => choice('□', '[]'),
+    sort   : $ => choice($.star, $.square, seq($.square, /[0-9]+/)),
 
     labs : $ => seq(
       choice('λ', 'fun'),
@@ -52,8 +53,7 @@ module.exports = grammar({
 
     term : $ => choice(
       $.identifier,
-      $.star,
-      $.square,
+      $.sort,
       seq('(', $.expr, ')'),
     ),
 
diff --git a/src/grammar.json b/src/grammar.json
index 07b841d..4920766 100644
--- a/src/grammar.json
+++ b/src/grammar.json
@@ -94,6 +94,32 @@
         }
       ]
     },
+    "sort": {
+      "type": "CHOICE",
+      "members": [
+        {
+          "type": "SYMBOL",
+          "name": "star"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "square"
+        },
+        {
+          "type": "SEQ",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "square"
+            },
+            {
+              "type": "PATTERN",
+              "value": "[0-9]+"
+            }
+          ]
+        }
+      ]
+    },
     "labs": {
       "type": "SEQ",
       "members": [
@@ -202,11 +228,7 @@
         },
         {
           "type": "SYMBOL",
-          "name": "star"
-        },
-        {
-          "type": "SYMBOL",
-          "name": "square"
+          "name": "sort"
         },
         {
           "type": "SEQ",
diff --git a/src/node-types.json b/src/node-types.json
index d1f34c5..7b03d9e 100644
--- a/src/node-types.json
+++ b/src/node-types.json
@@ -319,6 +319,25 @@
       ]
     }
   },
+  {
+    "type": "sort",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": false,
+      "required": true,
+      "types": [
+        {
+          "type": "square",
+          "named": true
+        },
+        {
+          "type": "star",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "square",
     "named": true,
@@ -341,11 +360,7 @@
           "named": true
         },
         {
-          "type": "square",
-          "named": true
-        },
-        {
-          "type": "star",
+          "type": "sort",
           "named": true
         }
       ]
diff --git a/src/parser.c b/src/parser.c
index 40e434f..3a233bd 100644
--- a/src/parser.c
+++ b/src/parser.c
@@ -5,11 +5,11 @@
 #endif
 
 #define LANGUAGE_VERSION 14
-#define STATE_COUNT 102
+#define STATE_COUNT 108
 #define LARGE_STATE_COUNT 2
-#define SYMBOL_COUNT 48
+#define SYMBOL_COUNT 50
 #define ALIAS_COUNT 0
-#define TOKEN_COUNT 27
+#define TOKEN_COUNT 28
 #define EXTERNAL_TOKEN_COUNT 0
 #define FIELD_COUNT 3
 #define MAX_ALIAS_SEQUENCE_LENGTH 7
@@ -24,45 +24,47 @@ enum ts_symbol_identifiers {
   sym_star = 6,
   anon_sym_u25a1 = 7,
   anon_sym_LBRACK_RBRACK = 8,
-  anon_sym_u03bb = 9,
-  anon_sym_fun = 10,
-  anon_sym_EQ_GT = 11,
-  anon_sym_u21d2 = 12,
-  anon_sym_u220f = 13,
-  anon_sym_forall = 14,
-  anon_sym_COMMA = 15,
-  anon_sym_COLON_EQ = 16,
-  anon_sym_let = 17,
-  anon_sym_in = 18,
-  anon_sym_end = 19,
-  anon_sym_DASH_GT = 20,
-  anon_sym_u2192 = 21,
-  anon_sym_axiom = 22,
-  anon_sym_SEMI = 23,
-  anon_sym_def = 24,
-  sym_post_command = 25,
-  sym_command = 26,
-  sym_program = 27,
-  sym_param_block = 28,
-  sym_square = 29,
-  sym_labs = 30,
-  sym_pabs = 31,
-  sym_term = 32,
-  sym_binding = 33,
-  sym_let = 34,
-  sym_app = 35,
-  sym_arrow = 36,
-  sym_app_term = 37,
-  sym_expr = 38,
-  sym_ascription = 39,
-  sym_axiom = 40,
-  sym_definition = 41,
-  sym_preprocess = 42,
-  aux_sym_program_repeat1 = 43,
-  aux_sym_param_block_repeat1 = 44,
-  aux_sym_labs_repeat1 = 45,
-  aux_sym_let_repeat1 = 46,
-  aux_sym_app_repeat1 = 47,
+  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,
 };
 
 static const char * const ts_symbol_names[] = {
@@ -75,6 +77,7 @@ static const char * const ts_symbol_names[] = {
   [sym_star] = "star",
   [anon_sym_u25a1] = "\u25a1",
   [anon_sym_LBRACK_RBRACK] = "[]",
+  [aux_sym_sort_token1] = "sort_token1",
   [anon_sym_u03bb] = "\u03bb",
   [anon_sym_fun] = "fun",
   [anon_sym_EQ_GT] = "=>",
@@ -96,6 +99,7 @@ static const char * const ts_symbol_names[] = {
   [sym_program] = "program",
   [sym_param_block] = "param_block",
   [sym_square] = "square",
+  [sym_sort] = "sort",
   [sym_labs] = "labs",
   [sym_pabs] = "pabs",
   [sym_term] = "term",
@@ -126,6 +130,7 @@ static const TSSymbol ts_symbol_map[] = {
   [sym_star] = sym_star,
   [anon_sym_u25a1] = anon_sym_u25a1,
   [anon_sym_LBRACK_RBRACK] = anon_sym_LBRACK_RBRACK,
+  [aux_sym_sort_token1] = aux_sym_sort_token1,
   [anon_sym_u03bb] = anon_sym_u03bb,
   [anon_sym_fun] = anon_sym_fun,
   [anon_sym_EQ_GT] = anon_sym_EQ_GT,
@@ -147,6 +152,7 @@ static const TSSymbol ts_symbol_map[] = {
   [sym_program] = sym_program,
   [sym_param_block] = sym_param_block,
   [sym_square] = sym_square,
+  [sym_sort] = sym_sort,
   [sym_labs] = sym_labs,
   [sym_pabs] = sym_pabs,
   [sym_term] = sym_term,
@@ -204,6 +210,10 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
+  [aux_sym_sort_token1] = {
+    .visible = false,
+    .named = false,
+  },
   [anon_sym_u03bb] = {
     .visible = true,
     .named = false,
@@ -288,6 +298,10 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = true,
   },
+  [sym_sort] = {
+    .visible = true,
+    .named = true,
+  },
   [sym_labs] = {
     .visible = true,
     .named = true,
@@ -414,25 +428,25 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [11] = 11,
   [12] = 12,
   [13] = 13,
-  [14] = 14,
+  [14] = 3,
   [15] = 15,
-  [16] = 7,
-  [17] = 2,
+  [16] = 16,
+  [17] = 17,
   [18] = 9,
   [19] = 11,
-  [20] = 12,
-  [21] = 4,
-  [22] = 22,
+  [20] = 2,
+  [21] = 13,
+  [22] = 6,
   [23] = 23,
   [24] = 24,
   [25] = 25,
   [26] = 26,
   [27] = 27,
-  [28] = 24,
-  [29] = 23,
+  [28] = 28,
+  [29] = 29,
   [30] = 30,
-  [31] = 31,
-  [32] = 32,
+  [31] = 24,
+  [32] = 23,
   [33] = 33,
   [34] = 34,
   [35] = 35,
@@ -440,26 +454,26 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [37] = 37,
   [38] = 38,
   [39] = 39,
-  [40] = 25,
-  [41] = 27,
-  [42] = 26,
+  [40] = 26,
+  [41] = 25,
+  [42] = 42,
   [43] = 43,
   [44] = 44,
-  [45] = 45,
-  [46] = 45,
+  [45] = 28,
+  [46] = 30,
   [47] = 47,
-  [48] = 48,
-  [49] = 49,
+  [48] = 27,
+  [49] = 29,
   [50] = 50,
   [51] = 51,
-  [52] = 52,
-  [53] = 51,
+  [52] = 51,
+  [53] = 53,
   [54] = 54,
   [55] = 55,
   [56] = 56,
   [57] = 57,
   [58] = 58,
-  [59] = 59,
+  [59] = 58,
   [60] = 60,
   [61] = 61,
   [62] = 62,
@@ -468,23 +482,23 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [65] = 65,
   [66] = 66,
   [67] = 67,
-  [68] = 65,
+  [68] = 68,
   [69] = 69,
-  [70] = 44,
+  [70] = 70,
   [71] = 71,
-  [72] = 66,
+  [72] = 72,
   [73] = 73,
   [74] = 74,
   [75] = 75,
-  [76] = 76,
-  [77] = 77,
+  [76] = 44,
+  [77] = 72,
   [78] = 73,
   [79] = 79,
   [80] = 80,
   [81] = 81,
   [82] = 82,
   [83] = 83,
-  [84] = 84,
+  [84] = 83,
   [85] = 85,
   [86] = 86,
   [87] = 87,
@@ -494,14 +508,20 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [91] = 91,
   [92] = 92,
   [93] = 93,
-  [94] = 85,
+  [94] = 94,
   [95] = 95,
   [96] = 96,
   [97] = 97,
-  [98] = 87,
+  [98] = 98,
   [99] = 99,
   [100] = 100,
   [101] = 101,
+  [102] = 102,
+  [103] = 100,
+  [104] = 97,
+  [105] = 105,
+  [106] = 106,
+  [107] = 107,
 };
 
 static bool ts_lex(TSLexer *lexer, TSStateId state) {
@@ -514,10 +534,10 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
         '(', 46,
         ')', 48,
         '*', 49,
-        ',', 60,
+        ',', 61,
         '-', 6,
         ':', 47,
-        ';', 70,
+        ';', 71,
         '=', 7,
         '@', 18,
         '[', 8,
@@ -527,39 +547,41 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
         'f', 27,
         'i', 24,
         'l', 14,
-        0x3bb, 52,
-        0x2192, 68,
-        0x21d2, 56,
-        0x220f, 57,
+        0x3bb, 53,
+        0x2192, 69,
+        0x21d2, 57,
+        0x220f, 58,
         0x25a1, 50,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(0);
+      if (('0' <= lookahead && lookahead <= '9')) ADVANCE(52);
       END_STATE();
     case 1:
       if (lookahead == '\n') SKIP(1);
-      if (lookahead == '-') ADVANCE(72);
+      if (lookahead == '-') ADVANCE(73);
       if (('\t' <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') ADVANCE(73);
-      if (lookahead != 0) ADVANCE(74);
+          lookahead == ' ') ADVANCE(74);
+      if (lookahead != 0) ADVANCE(75);
       END_STATE();
     case 2:
       ADVANCE_MAP(
         '(', 46,
         ')', 48,
         '*', 49,
-        ',', 60,
+        ',', 61,
         '-', 6,
         ':', 47,
-        ';', 70,
+        ';', 71,
         '=', 7,
         '[', 8,
-        0x2192, 68,
-        0x21d2, 56,
+        0x2192, 69,
+        0x21d2, 57,
         0x25a1, 50,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(2);
+      if (('0' <= lookahead && lookahead <= '9')) ADVANCE(52);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
           ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
@@ -570,10 +592,11 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == '-') ADVANCE(6);
       if (lookahead == '[') ADVANCE(8);
       if (lookahead == 'e') ADVANCE(40);
-      if (lookahead == 0x2192) ADVANCE(68);
+      if (lookahead == 0x2192) ADVANCE(69);
       if (lookahead == 0x25a1) ADVANCE(50);
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(3);
+      if (('0' <= lookahead && lookahead <= '9')) ADVANCE(52);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
           ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
@@ -586,8 +609,8 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
         '[', 8,
         'f', 41,
         'l', 36,
-        0x3bb, 52,
-        0x220f, 57,
+        0x3bb, 53,
+        0x220f, 58,
         0x25a1, 50,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
@@ -601,10 +624,10 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 6:
       if (lookahead == '-') ADVANCE(45);
-      if (lookahead == '>') ADVANCE(67);
+      if (lookahead == '>') ADVANCE(68);
       END_STATE();
     case 7:
-      if (lookahead == '>') ADVANCE(55);
+      if (lookahead == '>') ADVANCE(56);
       END_STATE();
     case 8:
       if (lookahead == ']') ADVANCE(51);
@@ -616,7 +639,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == 'c') ADVANCE(19);
       END_STATE();
     case 11:
-      if (lookahead == 'd') ADVANCE(65);
+      if (lookahead == 'd') ADVANCE(66);
       END_STATE();
     case 12:
       if (lookahead == 'd') ADVANCE(15);
@@ -628,10 +651,10 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == 'e') ADVANCE(30);
       END_STATE();
     case 15:
-      if (lookahead == 'e') ADVANCE(75);
+      if (lookahead == 'e') ADVANCE(76);
       END_STATE();
     case 16:
-      if (lookahead == 'f') ADVANCE(71);
+      if (lookahead == 'f') ADVANCE(72);
       END_STATE();
     case 17:
       if (lookahead == 'i') ADVANCE(28);
@@ -643,25 +666,25 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == 'l') ADVANCE(31);
       END_STATE();
     case 20:
-      if (lookahead == 'l') ADVANCE(58);
+      if (lookahead == 'l') ADVANCE(59);
       END_STATE();
     case 21:
       if (lookahead == 'l') ADVANCE(20);
       END_STATE();
     case 22:
-      if (lookahead == 'm') ADVANCE(69);
+      if (lookahead == 'm') ADVANCE(70);
       END_STATE();
     case 23:
       if (lookahead == 'n') ADVANCE(11);
       END_STATE();
     case 24:
-      if (lookahead == 'n') ADVANCE(64);
+      if (lookahead == 'n') ADVANCE(65);
       END_STATE();
     case 25:
       if (lookahead == 'n') ADVANCE(10);
       END_STATE();
     case 26:
-      if (lookahead == 'n') ADVANCE(53);
+      if (lookahead == 'n') ADVANCE(54);
       END_STATE();
     case 27:
       if (lookahead == 'o') ADVANCE(29);
@@ -674,7 +697,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == 'r') ADVANCE(9);
       END_STATE();
     case 30:
-      if (lookahead == 't') ADVANCE(62);
+      if (lookahead == 't') ADVANCE(63);
       END_STATE();
     case 31:
       if (lookahead == 'u') ADVANCE(12);
@@ -695,7 +718,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 35:
       ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'd') ADVANCE(66);
+      if (lookahead == 'd') ADVANCE(67);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
@@ -711,7 +734,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 37:
       ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'l') ADVANCE(59);
+      if (lookahead == 'l') ADVANCE(60);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
@@ -727,7 +750,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 39:
       ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'n') ADVANCE(54);
+      if (lookahead == 'n') ADVANCE(55);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
@@ -760,7 +783,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 43:
       ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 't') ADVANCE(63);
+      if (lookahead == 't') ADVANCE(64);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
@@ -783,7 +806,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 47:
       ACCEPT_TOKEN(anon_sym_COLON);
-      if (lookahead == '=') ADVANCE(61);
+      if (lookahead == '=') ADVANCE(62);
       END_STATE();
     case 48:
       ACCEPT_TOKEN(anon_sym_RPAREN);
@@ -798,102 +821,106 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK);
       END_STATE();
     case 52:
-      ACCEPT_TOKEN(anon_sym_u03bb);
+      ACCEPT_TOKEN(aux_sym_sort_token1);
+      if (('0' <= lookahead && lookahead <= '9')) ADVANCE(52);
       END_STATE();
     case 53:
-      ACCEPT_TOKEN(anon_sym_fun);
+      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 55:
+    case 56:
       ACCEPT_TOKEN(anon_sym_EQ_GT);
       END_STATE();
-    case 56:
+    case 57:
       ACCEPT_TOKEN(anon_sym_u21d2);
       END_STATE();
-    case 57:
-      ACCEPT_TOKEN(anon_sym_u220f);
-      END_STATE();
     case 58:
-      ACCEPT_TOKEN(anon_sym_forall);
+      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 60:
+    case 61:
       ACCEPT_TOKEN(anon_sym_COMMA);
       END_STATE();
-    case 61:
-      ACCEPT_TOKEN(anon_sym_COLON_EQ);
-      END_STATE();
     case 62:
-      ACCEPT_TOKEN(anon_sym_let);
+      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 64:
-      ACCEPT_TOKEN(anon_sym_in);
-      END_STATE();
     case 65:
-      ACCEPT_TOKEN(anon_sym_end);
+      ACCEPT_TOKEN(anon_sym_in);
       END_STATE();
     case 66:
+      ACCEPT_TOKEN(anon_sym_end);
+      END_STATE();
+    case 67:
       ACCEPT_TOKEN(anon_sym_end);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
           ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
       END_STATE();
-    case 67:
+    case 68:
       ACCEPT_TOKEN(anon_sym_DASH_GT);
       END_STATE();
-    case 68:
+    case 69:
       ACCEPT_TOKEN(anon_sym_u2192);
       END_STATE();
-    case 69:
+    case 70:
       ACCEPT_TOKEN(anon_sym_axiom);
       END_STATE();
-    case 70:
+    case 71:
       ACCEPT_TOKEN(anon_sym_SEMI);
       END_STATE();
-    case 71:
-      ACCEPT_TOKEN(anon_sym_def);
-      END_STATE();
     case 72:
-      ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '-') ADVANCE(45);
-      if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(74);
+      ACCEPT_TOKEN(anon_sym_def);
       END_STATE();
     case 73:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '-') ADVANCE(72);
-      if (lookahead == '\t' ||
-          (0x0b <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') ADVANCE(73);
+      if (lookahead == '-') ADVANCE(45);
       if (lookahead != 0 &&
-          (lookahead < '\t' || '\r' < lookahead)) ADVANCE(74);
+          lookahead != '\n') ADVANCE(75);
       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 != '\n') ADVANCE(74);
+          (lookahead < '\t' || '\r' < lookahead)) ADVANCE(75);
       END_STATE();
     case 75:
+      ACCEPT_TOKEN(sym_post_command);
+      if (lookahead != 0 &&
+          lookahead != '\n') ADVANCE(75);
+      END_STATE();
+    case 76:
       ACCEPT_TOKEN(sym_command);
       END_STATE();
     default:
@@ -930,11 +957,11 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [25] = {.lex_state = 2},
   [26] = {.lex_state = 2},
   [27] = {.lex_state = 2},
-  [28] = {.lex_state = 3},
-  [29] = {.lex_state = 3},
-  [30] = {.lex_state = 0},
-  [31] = {.lex_state = 0},
-  [32] = {.lex_state = 0},
+  [28] = {.lex_state = 2},
+  [29] = {.lex_state = 2},
+  [30] = {.lex_state = 2},
+  [31] = {.lex_state = 3},
+  [32] = {.lex_state = 3},
   [33] = {.lex_state = 0},
   [34] = {.lex_state = 0},
   [35] = {.lex_state = 0},
@@ -944,14 +971,14 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [39] = {.lex_state = 0},
   [40] = {.lex_state = 3},
   [41] = {.lex_state = 3},
-  [42] = {.lex_state = 3},
+  [42] = {.lex_state = 0},
   [43] = {.lex_state = 0},
   [44] = {.lex_state = 0},
-  [45] = {.lex_state = 0},
-  [46] = {.lex_state = 0},
+  [45] = {.lex_state = 3},
+  [46] = {.lex_state = 3},
   [47] = {.lex_state = 0},
-  [48] = {.lex_state = 0},
-  [49] = {.lex_state = 0},
+  [48] = {.lex_state = 3},
+  [49] = {.lex_state = 3},
   [50] = {.lex_state = 0},
   [51] = {.lex_state = 0},
   [52] = {.lex_state = 0},
@@ -971,39 +998,45 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [66] = {.lex_state = 0},
   [67] = {.lex_state = 0},
   [68] = {.lex_state = 0},
-  [69] = {.lex_state = 2},
+  [69] = {.lex_state = 0},
   [70] = {.lex_state = 0},
   [71] = {.lex_state = 2},
   [72] = {.lex_state = 0},
   [73] = {.lex_state = 0},
-  [74] = {.lex_state = 2},
-  [75] = {.lex_state = 0},
+  [74] = {.lex_state = 0},
+  [75] = {.lex_state = 2},
   [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 = 0},
+  [82] = {.lex_state = 2},
   [83] = {.lex_state = 0},
   [84] = {.lex_state = 0},
   [85] = {.lex_state = 0},
   [86] = {.lex_state = 0},
   [87] = {.lex_state = 0},
-  [88] = {.lex_state = 2},
+  [88] = {.lex_state = 0},
   [89] = {.lex_state = 0},
-  [90] = {.lex_state = 2},
-  [91] = {.lex_state = 0},
+  [90] = {.lex_state = 0},
+  [91] = {.lex_state = 2},
   [92] = {.lex_state = 0},
   [93] = {.lex_state = 0},
-  [94] = {.lex_state = 0},
-  [95] = {.lex_state = 1},
+  [94] = {.lex_state = 2},
+  [95] = {.lex_state = 0},
   [96] = {.lex_state = 2},
   [97] = {.lex_state = 0},
   [98] = {.lex_state = 0},
   [99] = {.lex_state = 0},
   [100] = {.lex_state = 0},
-  [101] = {.lex_state = 0},
+  [101] = {.lex_state = 1},
+  [102] = {.lex_state = 0},
+  [103] = {.lex_state = 0},
+  [104] = {.lex_state = 0},
+  [105] = {.lex_state = 0},
+  [106] = {.lex_state = 0},
+  [107] = {.lex_state = 0},
 };
 
 static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
@@ -1016,6 +1049,7 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
     [sym_star] = ACTIONS(1),
     [anon_sym_u25a1] = ACTIONS(1),
     [anon_sym_LBRACK_RBRACK] = ACTIONS(1),
+    [aux_sym_sort_token1] = ACTIONS(1),
     [anon_sym_u03bb] = ACTIONS(1),
     [anon_sym_fun] = ACTIONS(1),
     [anon_sym_EQ_GT] = ACTIONS(1),
@@ -1035,11 +1069,11 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
     [sym_command] = ACTIONS(1),
   },
   [1] = {
-    [sym_program] = STATE(83),
-    [sym_axiom] = STATE(38),
-    [sym_definition] = STATE(38),
-    [sym_preprocess] = STATE(38),
-    [aux_sym_program_repeat1] = STATE(38),
+    [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_comment] = ACTIONS(3),
     [anon_sym_axiom] = ACTIONS(7),
@@ -1049,7 +1083,7 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
 };
 
 static const uint16_t ts_small_parse_table[] = {
-  [0] = 16,
+  [0] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1070,9 +1104,11 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_let,
     STATE(25), 1,
       sym_square,
-    STATE(34), 1,
+    STATE(28), 1,
+      sym_sort,
+    STATE(35), 1,
       sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
     STATE(44), 1,
       sym_app_term,
@@ -1087,7 +1123,47 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [54] = 16,
+  [57] = 17,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(29), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_identifier,
+    ACTIONS(33), 1,
+      anon_sym_LPAREN,
+    ACTIONS(35), 1,
+      sym_star,
+    ACTIONS(39), 1,
+      anon_sym_u03bb,
+    ACTIONS(41), 1,
+      anon_sym_fun,
+    ACTIONS(43), 1,
+      anon_sym_u220f,
+    ACTIONS(45), 1,
+      anon_sym_forall,
+    STATE(37), 1,
+      sym_expr,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(41), 1,
+      sym_square,
+    STATE(45), 1,
+      sym_sort,
+    STATE(76), 1,
+      sym_app_term,
+    ACTIONS(37), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(31), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [114] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1108,7 +1184,169 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_let,
     STATE(25), 1,
       sym_square,
-    STATE(37), 1,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(62), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(86), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(103), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(90), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
       sym_arrow,
     STATE(44), 1,
       sym_app_term,
@@ -1125,197 +1363,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [108] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(85), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [162] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(99), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [216] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(80), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [270] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(32), 1,
-      sym_expr,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [324] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(82), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [378] = 16,
+  [399] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1336,9 +1384,11 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_let,
     STATE(25), 1,
       sym_square,
+    STATE(28), 1,
+      sym_sort,
     STATE(33), 1,
       sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
     STATE(44), 1,
       sym_app_term,
@@ -1353,7 +1403,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [432] = 16,
+  [456] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1374,11 +1424,13 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_let,
     STATE(25), 1,
       sym_square,
-    STATE(37), 1,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
       sym_arrow,
     STATE(44), 1,
       sym_app_term,
-    STATE(54), 1,
+    STATE(98), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
@@ -1391,7 +1443,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [486] = 16,
+  [513] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1412,9 +1464,11 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_let,
     STATE(25), 1,
       sym_square,
-    STATE(30), 1,
+    STATE(28), 1,
+      sym_sort,
+    STATE(34), 1,
       sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
     STATE(44), 1,
       sym_app_term,
@@ -1429,159 +1483,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [540] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(31), 1,
-      sym_expr,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [594] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(91), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [648] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(97), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [702] = 16,
-    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,
-      anon_sym_let,
-    STATE(25), 1,
-      sym_square,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(44), 1,
-      sym_app_term,
-    STATE(81), 1,
-      sym_expr,
-    ACTIONS(19), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(24), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [756] = 16,
+  [570] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(29), 1,
@@ -1600,18 +1502,20 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(45), 1,
       anon_sym_forall,
-    STATE(32), 1,
-      sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
-    STATE(40), 1,
+    STATE(41), 1,
       sym_square,
-    STATE(70), 1,
+    STATE(45), 1,
+      sym_sort,
+    STATE(76), 1,
       sym_app_term,
+    STATE(107), 1,
+      sym_expr,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(28), 2,
+    STATE(31), 2,
       sym_term,
       aux_sym_app_repeat1,
     STATE(36), 4,
@@ -1619,7 +1523,247 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [810] = 16,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(39), 1,
+      sym_expr,
+    STATE(44), 1,
+      sym_app_term,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(37), 1,
+      sym_expr,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(93), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [798] = 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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(85), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [855] = 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,
+      anon_sym_let,
+    STATE(25), 1,
+      sym_square,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
+    STATE(106), 1,
+      sym_expr,
+    ACTIONS(19), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(24), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [912] = 17,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(29), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_identifier,
+    ACTIONS(33), 1,
+      anon_sym_LPAREN,
+    ACTIONS(35), 1,
+      sym_star,
+    ACTIONS(39), 1,
+      anon_sym_u03bb,
+    ACTIONS(41), 1,
+      anon_sym_fun,
+    ACTIONS(43), 1,
+      anon_sym_u220f,
+    ACTIONS(45), 1,
+      anon_sym_forall,
+    STATE(33), 1,
+      sym_expr,
+    STATE(38), 1,
+      sym_arrow,
+    STATE(41), 1,
+      sym_square,
+    STATE(45), 1,
+      sym_sort,
+    STATE(76), 1,
+      sym_app_term,
+    ACTIONS(37), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(31), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [969] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(29), 1,
@@ -1640,16 +1784,18 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     STATE(34), 1,
       sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
-    STATE(40), 1,
+    STATE(41), 1,
       sym_square,
-    STATE(70), 1,
+    STATE(45), 1,
+      sym_sort,
+    STATE(76), 1,
       sym_app_term,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(28), 2,
+    STATE(31), 2,
       sym_term,
       aux_sym_app_repeat1,
     STATE(36), 4,
@@ -1657,7 +1803,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [864] = 16,
+  [1026] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(29), 1,
@@ -1676,18 +1822,20 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(45), 1,
       anon_sym_forall,
-    STATE(33), 1,
+    STATE(35), 1,
       sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
-    STATE(40), 1,
+    STATE(41), 1,
       sym_square,
-    STATE(70), 1,
+    STATE(45), 1,
+      sym_sort,
+    STATE(76), 1,
       sym_app_term,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(28), 2,
+    STATE(31), 2,
       sym_term,
       aux_sym_app_repeat1,
     STATE(36), 4,
@@ -1695,7 +1843,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [918] = 16,
+  [1083] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(29), 1,
@@ -1714,18 +1862,20 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(45), 1,
       anon_sym_forall,
-    STATE(30), 1,
-      sym_expr,
-    STATE(37), 1,
+    STATE(38), 1,
       sym_arrow,
-    STATE(40), 1,
+    STATE(39), 1,
+      sym_expr,
+    STATE(41), 1,
       sym_square,
-    STATE(70), 1,
+    STATE(45), 1,
+      sym_sort,
+    STATE(76), 1,
       sym_app_term,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(28), 2,
+    STATE(31), 2,
       sym_term,
       aux_sym_app_repeat1,
     STATE(36), 4,
@@ -1733,45 +1883,7 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [972] = 16,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
-    ACTIONS(31), 1,
-      sym_identifier,
-    ACTIONS(33), 1,
-      anon_sym_LPAREN,
-    ACTIONS(35), 1,
-      sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
-    ACTIONS(41), 1,
-      anon_sym_fun,
-    ACTIONS(43), 1,
-      anon_sym_u220f,
-    ACTIONS(45), 1,
-      anon_sym_forall,
-    STATE(31), 1,
-      sym_expr,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(40), 1,
-      sym_square,
-    STATE(70), 1,
-      sym_app_term,
-    ACTIONS(37), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(28), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [1026] = 16,
+  [1140] = 17,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1792,11 +1904,13 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_let,
     STATE(25), 1,
       sym_square,
-    STATE(37), 1,
+    STATE(28), 1,
+      sym_sort,
+    STATE(38), 1,
       sym_arrow,
     STATE(44), 1,
       sym_app_term,
-    STATE(94), 1,
+    STATE(100), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
@@ -1809,55 +1923,20 @@ static const uint16_t ts_small_parse_table[] = {
       sym_pabs,
       sym_let,
       sym_app,
-  [1080] = 16,
+  [1197] = 9,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(29), 1,
-      anon_sym_let,
-    ACTIONS(31), 1,
+    ACTIONS(47), 1,
       sym_identifier,
-    ACTIONS(33), 1,
-      anon_sym_LPAREN,
-    ACTIONS(35), 1,
-      sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
-    ACTIONS(41), 1,
-      anon_sym_fun,
-    ACTIONS(43), 1,
-      anon_sym_u220f,
-    ACTIONS(45), 1,
-      anon_sym_forall,
-    STATE(37), 1,
-      sym_arrow,
-    STATE(40), 1,
-      sym_square,
-    STATE(70), 1,
-      sym_app_term,
-    STATE(84), 1,
-      sym_expr,
-    ACTIONS(37), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(28), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(36), 4,
-      sym_labs,
-      sym_pabs,
-      sym_let,
-      sym_app,
-  [1134] = 7,
-    ACTIONS(3), 1,
-      sym_comment,
     ACTIONS(50), 1,
       anon_sym_LPAREN,
+    ACTIONS(55), 1,
+      sym_star,
     STATE(25), 1,
       sym_square,
-    ACTIONS(47), 2,
-      sym_identifier,
-      sym_star,
-    ACTIONS(55), 2,
+    STATE(28), 1,
+      sym_sort,
+    ACTIONS(58), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
     STATE(23), 2,
@@ -1872,23 +1951,26 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1166] = 7,
+  [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,
-    ACTIONS(17), 2,
-      sym_identifier,
-      sym_star,
+    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(58), 8,
+    ACTIONS(63), 8,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -1897,10 +1979,12 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1198] = 2,
+  [1271] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(60), 13,
+    ACTIONS(67), 1,
+      aux_sym_sort_token1,
+    ACTIONS(65), 13,
       sym_identifier,
       anon_sym_LPAREN,
       anon_sym_RPAREN,
@@ -1914,10 +1998,28 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1217] = 2,
+  [1293] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(62), 13,
+    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,
@@ -1931,10 +2033,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1236] = 2,
+  [1332] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(64), 13,
+    ACTIONS(73), 13,
       sym_identifier,
       anon_sym_LPAREN,
       anon_sym_RPAREN,
@@ -1948,7 +2050,41 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1255] = 9,
+  [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,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(31), 1,
@@ -1957,45 +2093,49 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_LPAREN,
     ACTIONS(35), 1,
       sym_star,
-    ACTIONS(66), 1,
+    ACTIONS(77), 1,
       anon_sym_end,
-    STATE(40), 1,
+    STATE(41), 1,
       sym_square,
+    STATE(45), 1,
+      sym_sort,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    ACTIONS(58), 2,
+    ACTIONS(63), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-    STATE(29), 2,
+    STATE(32), 2,
       sym_term,
       aux_sym_app_repeat1,
-  [1286] = 9,
+  [1423] = 10,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(68), 1,
+    ACTIONS(79), 1,
       sym_identifier,
-    ACTIONS(71), 1,
+    ACTIONS(82), 1,
       anon_sym_LPAREN,
-    ACTIONS(74), 1,
+    ACTIONS(85), 1,
       sym_star,
-    ACTIONS(80), 1,
+    ACTIONS(91), 1,
       anon_sym_end,
-    STATE(40), 1,
+    STATE(41), 1,
       sym_square,
+    STATE(45), 1,
+      sym_sort,
     ACTIONS(53), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-    ACTIONS(77), 2,
+    ACTIONS(88), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(29), 2,
+    STATE(32), 2,
       sym_term,
       aux_sym_app_repeat1,
-  [1317] = 2,
+  [1457] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(82), 9,
+    ACTIONS(93), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2005,10 +2145,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1332] = 2,
+  [1472] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(84), 9,
+    ACTIONS(95), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2018,10 +2158,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1347] = 2,
+  [1487] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(86), 9,
+    ACTIONS(97), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2031,10 +2171,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1362] = 2,
+  [1502] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(88), 9,
+    ACTIONS(99), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2044,10 +2184,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1377] = 2,
+  [1517] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(90), 9,
+    ACTIONS(101), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2057,10 +2197,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1392] = 2,
+  [1532] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(92), 9,
+    ACTIONS(103), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2070,10 +2210,10 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1407] = 2,
+  [1547] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(94), 9,
+    ACTIONS(105), 9,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
@@ -2083,10 +2223,39 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1422] = 2,
+  [1562] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(96), 9,
+    ACTIONS(107), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(69), 7,
+      anon_sym_LPAREN,
+      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,
@@ -2096,7 +2265,7 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_DASH_GT,
       anon_sym_u2192,
       anon_sym_SEMI,
-  [1437] = 6,
+  [1613] = 6,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(7), 1,
@@ -2105,307 +2274,268 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_def,
     ACTIONS(11), 1,
       sym_command,
-    ACTIONS(98), 1,
-      ts_builtin_sym_end,
-    STATE(43), 4,
-      sym_axiom,
-      sym_definition,
-      sym_preprocess,
-      aux_sym_program_repeat1,
-  [1459] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(100), 1,
-      anon_sym_LPAREN,
-    ACTIONS(103), 1,
-      anon_sym_COLON,
-    STATE(39), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-    ACTIONS(105), 4,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-  [1479] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(107), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(60), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1495] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(109), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(64), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1511] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(111), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(62), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1527] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(113), 1,
-      ts_builtin_sym_end,
     ACTIONS(115), 1,
-      anon_sym_axiom,
-    ACTIONS(118), 1,
-      anon_sym_def,
-    ACTIONS(121), 1,
-      sym_command,
-    STATE(43), 4,
+      ts_builtin_sym_end,
+    STATE(50), 4,
       sym_axiom,
       sym_definition,
       sym_preprocess,
       aux_sym_program_repeat1,
-  [1549] = 3,
+  [1635] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(124), 2,
+    ACTIONS(117), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-    ACTIONS(96), 6,
+    ACTIONS(103), 6,
       anon_sym_RPAREN,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
       anon_sym_COMMA,
       anon_sym_COLON_EQ,
       anon_sym_SEMI,
-  [1565] = 6,
+  [1651] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
+    ACTIONS(119), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(73), 6,
       anon_sym_LPAREN,
-    ACTIONS(128), 1,
+      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(73), 1,
-      sym_ascription,
+    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,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(39), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1586] = 6,
+      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(126), 1,
-      anon_sym_LPAREN,
-    ACTIONS(128), 1,
-      anon_sym_COLON,
-    STATE(78), 1,
-      sym_ascription,
-    ACTIONS(132), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(39), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1607] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(126), 1,
-      anon_sym_LPAREN,
+    ACTIONS(132), 1,
+      ts_builtin_sym_end,
     ACTIONS(134), 1,
-      anon_sym_COLON,
-    ACTIONS(136), 1,
-      anon_sym_COLON_EQ,
-    STATE(101), 1,
-      sym_ascription,
-    STATE(50), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1627] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
+      anon_sym_axiom,
+    ACTIONS(137), 1,
+      anon_sym_def,
     ACTIONS(140), 1,
-      anon_sym_COLON,
-    ACTIONS(138), 5,
+      sym_command,
+    STATE(50), 4,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1757] = 6,
+    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,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-  [1641] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(126), 1,
-      anon_sym_LPAREN,
-    ACTIONS(134), 1,
-      anon_sym_COLON,
-    ACTIONS(142), 1,
-      anon_sym_COLON_EQ,
-    STATE(86), 1,
-      sym_ascription,
-    STATE(52), 2,
+    STATE(47), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1661] = 6,
+  [1778] = 6,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
+    ACTIONS(143), 1,
       anon_sym_LPAREN,
-    ACTIONS(134), 1,
+    ACTIONS(145), 1,
       anon_sym_COLON,
-    ACTIONS(144), 1,
-      anon_sym_COLON_EQ,
-    STATE(93), 1,
+    STATE(84), 1,
       sym_ascription,
-    STATE(39), 2,
+    ACTIONS(149), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+    STATE(47), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1681] = 6,
+  [1799] = 6,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
+    ACTIONS(143), 1,
       anon_sym_LPAREN,
-    ACTIONS(128), 1,
+    ACTIONS(151), 1,
       anon_sym_COLON,
-    ACTIONS(146), 1,
-      anon_sym_COMMA,
+    ACTIONS(153), 1,
+      anon_sym_COLON_EQ,
     STATE(87), 1,
       sym_ascription,
-    STATE(39), 2,
+    STATE(56), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1701] = 6,
+  [1819] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
-      anon_sym_LPAREN,
-    ACTIONS(134), 1,
+    ACTIONS(157), 1,
       anon_sym_COLON,
-    ACTIONS(148), 1,
-      anon_sym_COLON_EQ,
-    STATE(100), 1,
-      sym_ascription,
-    STATE(39), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1721] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(126), 1,
+    ACTIONS(155), 5,
       anon_sym_LPAREN,
-    ACTIONS(128), 1,
-      anon_sym_COLON,
-    ACTIONS(150), 1,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
       anon_sym_COMMA,
-    STATE(98), 1,
-      sym_ascription,
-    STATE(39), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1741] = 2,
+      anon_sym_COLON_EQ,
+  [1833] = 6,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(152), 5,
+    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,
+      anon_sym_COMMA,
+    STATE(97), 1,
+      sym_ascription,
+    STATE(47), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1913] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(143), 1,
+      anon_sym_LPAREN,
+    ACTIONS(145), 1,
+      anon_sym_COLON,
+    ACTIONS(167), 1,
+      anon_sym_COMMA,
+    STATE(104), 1,
+      sym_ascription,
+    STATE(47), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1933] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(143), 1,
+      anon_sym_LPAREN,
+    ACTIONS(145), 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,
+      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,
-  [1752] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(126), 1,
-      anon_sym_LPAREN,
-    ACTIONS(128), 1,
-      anon_sym_COLON,
-    STATE(79), 1,
-      sym_ascription,
-    STATE(56), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1769] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(126), 1,
-      anon_sym_LPAREN,
-    ACTIONS(128), 1,
-      anon_sym_COLON,
-    STATE(89), 1,
-      sym_ascription,
-    STATE(39), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1786] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(154), 1,
-      anon_sym_LPAREN,
-    ACTIONS(157), 1,
-      anon_sym_in,
-    STATE(57), 2,
-      sym_binding,
-      aux_sym_let_repeat1,
-  [1800] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(159), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1810] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(161), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1820] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(163), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1830] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(165), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1840] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(167), 1,
-      anon_sym_LPAREN,
-    ACTIONS(169), 1,
-      anon_sym_in,
-    STATE(57), 2,
-      sym_binding,
-      aux_sym_let_repeat1,
-  [1854] = 2,
+  [1978] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(171), 4,
@@ -2413,335 +2543,393 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_axiom,
       anon_sym_def,
       sym_command,
-  [1864] = 2,
+  [1988] = 4,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(173), 4,
+    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,
-  [1874] = 3,
+  [2012] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
+    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,
-  [1885] = 3,
+  [2090] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
+    ACTIONS(143), 1,
       anon_sym_LPAREN,
-    STATE(45), 2,
+    STATE(58), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1896] = 3,
+  [2101] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(167), 1,
+    ACTIONS(173), 1,
       anon_sym_LPAREN,
-    STATE(62), 2,
+    STATE(64), 2,
       sym_binding,
       aux_sym_let_repeat1,
-  [1907] = 3,
+  [2112] = 4,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(126), 1,
-      anon_sym_LPAREN,
-    STATE(53), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1918] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(175), 1,
+    ACTIONS(197), 1,
       sym_identifier,
-    ACTIONS(177), 1,
+    ACTIONS(199), 1,
       anon_sym_COLON,
     STATE(71), 1,
       aux_sym_param_block_repeat1,
-  [1931] = 3,
+  [2125] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(96), 1,
+    ACTIONS(103), 1,
       anon_sym_end,
-    ACTIONS(179), 2,
+    ACTIONS(201), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-  [1942] = 4,
+  [2136] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(181), 1,
-      sym_identifier,
-    ACTIONS(184), 1,
-      anon_sym_COLON,
-    STATE(71), 1,
-      aux_sym_param_block_repeat1,
-  [1955] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(126), 1,
+    ACTIONS(143), 1,
       anon_sym_LPAREN,
-    STATE(46), 2,
+    STATE(52), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1966] = 2,
+  [2147] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(186), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-  [1974] = 3,
+    ACTIONS(143), 1,
+      anon_sym_LPAREN,
+    STATE(59), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [2158] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(188), 1,
+    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(69), 1,
+    STATE(75), 1,
       aux_sym_param_block_repeat1,
-  [1984] = 2,
+  [2192] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(190), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [1992] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(192), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [2000] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(194), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [2008] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(196), 2,
+    ACTIONS(211), 2,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
-  [2016] = 2,
+  [2200] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(198), 1,
-      anon_sym_SEMI,
-  [2023] = 2,
+    ACTIONS(213), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+  [2208] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(200), 1,
+    ACTIONS(215), 1,
       anon_sym_RPAREN,
-  [2030] = 2,
+  [2215] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(202), 1,
-      anon_sym_RPAREN,
-  [2037] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(204), 1,
+    ACTIONS(217), 1,
       anon_sym_SEMI,
-  [2044] = 2,
+  [2222] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(206), 1,
+    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,
+  [2271] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(231), 1,
+      sym_identifier,
+  [2278] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(233), 1,
+      anon_sym_COLON_EQ,
+  [2285] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(235), 1,
+      sym_identifier,
+  [2292] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(237), 1,
+      anon_sym_COMMA,
+  [2299] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(239), 1,
+      anon_sym_SEMI,
+  [2306] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(241), 1,
       ts_builtin_sym_end,
-  [2051] = 2,
+  [2313] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(208), 1,
-      anon_sym_end,
-  [2058] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(210), 1,
+    ACTIONS(243), 1,
       anon_sym_RPAREN,
-  [2065] = 2,
-    ACTIONS(3), 1,
+  [2320] = 2,
+    ACTIONS(245), 1,
       sym_comment,
-    ACTIONS(148), 1,
-      anon_sym_COLON_EQ,
-  [2072] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(212), 1,
-      anon_sym_COMMA,
-  [2079] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(214), 1,
-      sym_identifier,
-  [2086] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(216), 1,
-      anon_sym_SEMI,
-  [2093] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(218), 1,
-      sym_identifier,
-  [2100] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(220), 1,
-      anon_sym_RPAREN,
-  [2107] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(222), 1,
-      anon_sym_SEMI,
-  [2114] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(224), 1,
-      anon_sym_COLON_EQ,
-  [2121] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(226), 1,
-      anon_sym_RPAREN,
-  [2128] = 2,
-    ACTIONS(228), 1,
-      sym_comment,
-    ACTIONS(230), 1,
+    ACTIONS(247), 1,
       sym_post_command,
-  [2135] = 2,
+  [2327] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(232), 1,
-      sym_identifier,
-  [2142] = 2,
+    ACTIONS(163), 1,
+      anon_sym_COLON_EQ,
+  [2334] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(234), 1,
+    ACTIONS(249), 1,
       anon_sym_RPAREN,
-  [2149] = 2,
+  [2341] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(236), 1,
+    ACTIONS(251), 1,
       anon_sym_COMMA,
-  [2156] = 2,
+  [2348] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(238), 1,
+    ACTIONS(253), 1,
       anon_sym_SEMI,
-  [2163] = 2,
+  [2355] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(240), 1,
-      anon_sym_COLON_EQ,
-  [2170] = 2,
+    ACTIONS(255), 1,
+      anon_sym_RPAREN,
+  [2362] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(144), 1,
-      anon_sym_COLON_EQ,
+    ACTIONS(257), 1,
+      anon_sym_end,
 };
 
 static const uint32_t ts_small_parse_table_map[] = {
   [SMALL_STATE(2)] = 0,
-  [SMALL_STATE(3)] = 54,
-  [SMALL_STATE(4)] = 108,
-  [SMALL_STATE(5)] = 162,
-  [SMALL_STATE(6)] = 216,
-  [SMALL_STATE(7)] = 270,
-  [SMALL_STATE(8)] = 324,
-  [SMALL_STATE(9)] = 378,
-  [SMALL_STATE(10)] = 432,
-  [SMALL_STATE(11)] = 486,
-  [SMALL_STATE(12)] = 540,
-  [SMALL_STATE(13)] = 594,
-  [SMALL_STATE(14)] = 648,
-  [SMALL_STATE(15)] = 702,
-  [SMALL_STATE(16)] = 756,
-  [SMALL_STATE(17)] = 810,
-  [SMALL_STATE(18)] = 864,
-  [SMALL_STATE(19)] = 918,
-  [SMALL_STATE(20)] = 972,
-  [SMALL_STATE(21)] = 1026,
-  [SMALL_STATE(22)] = 1080,
-  [SMALL_STATE(23)] = 1134,
-  [SMALL_STATE(24)] = 1166,
-  [SMALL_STATE(25)] = 1198,
-  [SMALL_STATE(26)] = 1217,
-  [SMALL_STATE(27)] = 1236,
-  [SMALL_STATE(28)] = 1255,
-  [SMALL_STATE(29)] = 1286,
-  [SMALL_STATE(30)] = 1317,
-  [SMALL_STATE(31)] = 1332,
-  [SMALL_STATE(32)] = 1347,
-  [SMALL_STATE(33)] = 1362,
-  [SMALL_STATE(34)] = 1377,
-  [SMALL_STATE(35)] = 1392,
-  [SMALL_STATE(36)] = 1407,
-  [SMALL_STATE(37)] = 1422,
-  [SMALL_STATE(38)] = 1437,
-  [SMALL_STATE(39)] = 1459,
-  [SMALL_STATE(40)] = 1479,
-  [SMALL_STATE(41)] = 1495,
-  [SMALL_STATE(42)] = 1511,
-  [SMALL_STATE(43)] = 1527,
-  [SMALL_STATE(44)] = 1549,
-  [SMALL_STATE(45)] = 1565,
-  [SMALL_STATE(46)] = 1586,
-  [SMALL_STATE(47)] = 1607,
-  [SMALL_STATE(48)] = 1627,
-  [SMALL_STATE(49)] = 1641,
-  [SMALL_STATE(50)] = 1661,
-  [SMALL_STATE(51)] = 1681,
-  [SMALL_STATE(52)] = 1701,
-  [SMALL_STATE(53)] = 1721,
-  [SMALL_STATE(54)] = 1741,
-  [SMALL_STATE(55)] = 1752,
-  [SMALL_STATE(56)] = 1769,
-  [SMALL_STATE(57)] = 1786,
-  [SMALL_STATE(58)] = 1800,
-  [SMALL_STATE(59)] = 1810,
-  [SMALL_STATE(60)] = 1820,
-  [SMALL_STATE(61)] = 1830,
-  [SMALL_STATE(62)] = 1840,
-  [SMALL_STATE(63)] = 1854,
-  [SMALL_STATE(64)] = 1864,
-  [SMALL_STATE(65)] = 1874,
-  [SMALL_STATE(66)] = 1885,
-  [SMALL_STATE(67)] = 1896,
-  [SMALL_STATE(68)] = 1907,
-  [SMALL_STATE(69)] = 1918,
-  [SMALL_STATE(70)] = 1931,
-  [SMALL_STATE(71)] = 1942,
-  [SMALL_STATE(72)] = 1955,
-  [SMALL_STATE(73)] = 1966,
-  [SMALL_STATE(74)] = 1974,
-  [SMALL_STATE(75)] = 1984,
-  [SMALL_STATE(76)] = 1992,
-  [SMALL_STATE(77)] = 2000,
-  [SMALL_STATE(78)] = 2008,
-  [SMALL_STATE(79)] = 2016,
-  [SMALL_STATE(80)] = 2023,
-  [SMALL_STATE(81)] = 2030,
-  [SMALL_STATE(82)] = 2037,
-  [SMALL_STATE(83)] = 2044,
-  [SMALL_STATE(84)] = 2051,
-  [SMALL_STATE(85)] = 2058,
-  [SMALL_STATE(86)] = 2065,
-  [SMALL_STATE(87)] = 2072,
-  [SMALL_STATE(88)] = 2079,
-  [SMALL_STATE(89)] = 2086,
-  [SMALL_STATE(90)] = 2093,
-  [SMALL_STATE(91)] = 2100,
-  [SMALL_STATE(92)] = 2107,
-  [SMALL_STATE(93)] = 2114,
-  [SMALL_STATE(94)] = 2121,
-  [SMALL_STATE(95)] = 2128,
-  [SMALL_STATE(96)] = 2135,
-  [SMALL_STATE(97)] = 2142,
-  [SMALL_STATE(98)] = 2149,
-  [SMALL_STATE(99)] = 2156,
-  [SMALL_STATE(100)] = 2163,
-  [SMALL_STATE(101)] = 2170,
+  [SMALL_STATE(3)] = 57,
+  [SMALL_STATE(4)] = 114,
+  [SMALL_STATE(5)] = 171,
+  [SMALL_STATE(6)] = 228,
+  [SMALL_STATE(7)] = 285,
+  [SMALL_STATE(8)] = 342,
+  [SMALL_STATE(9)] = 399,
+  [SMALL_STATE(10)] = 456,
+  [SMALL_STATE(11)] = 513,
+  [SMALL_STATE(12)] = 570,
+  [SMALL_STATE(13)] = 627,
+  [SMALL_STATE(14)] = 684,
+  [SMALL_STATE(15)] = 741,
+  [SMALL_STATE(16)] = 798,
+  [SMALL_STATE(17)] = 855,
+  [SMALL_STATE(18)] = 912,
+  [SMALL_STATE(19)] = 969,
+  [SMALL_STATE(20)] = 1026,
+  [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,
 };
 
 static const TSParseActionEntry ts_parse_actions[] = {
@@ -2749,117 +2937,125 @@ static const TSParseActionEntry ts_parse_actions[] = {
   [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(90),
-  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(96),
-  [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(95),
-  [13] = {.entry = {.count = 1, .reusable = false}}, SHIFT(25),
-  [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4),
-  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(25),
+  [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(66),
-  [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(66),
-  [25] = {.entry = {.count = 1, .reusable = true}}, SHIFT(65),
-  [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(65),
-  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(67),
-  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(40),
-  [33] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21),
-  [35] = {.entry = {.count = 1, .reusable = true}}, SHIFT(40),
-  [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(42),
-  [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(72),
-  [41] = {.entry = {.count = 1, .reusable = false}}, SHIFT(72),
-  [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(68),
-  [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(68),
-  [47] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(25),
-  [50] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(4),
+  [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(26),
-  [58] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
-  [60] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
-  [62] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
-  [64] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
-  [66] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0),
-  [68] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(40),
-  [71] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(21),
-  [74] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(40),
-  [77] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(42),
-  [80] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
-  [82] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 5, 0, 0),
-  [84] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 5, 0, 0),
-  [86] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
-  [88] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
-  [90] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
-  [92] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0),
-  [94] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
-  [96] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
-  [98] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
-  [100] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(74),
-  [103] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [105] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [107] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0),
-  [109] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0),
-  [111] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0),
-  [113] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
-  [115] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(90),
-  [118] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(96),
-  [121] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(95),
-  [124] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
-  [126] = {.entry = {.count = 1, .reusable = true}}, SHIFT(74),
-  [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
-  [130] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
-  [132] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17),
-  [134] = {.entry = {.count = 1, .reusable = false}}, SHIFT(10),
-  [136] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13),
-  [138] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3),
-  [140] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3),
-  [142] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
-  [144] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
-  [146] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
-  [148] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5),
-  [150] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18),
-  [152] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
-  [154] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(88),
-  [157] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0),
-  [159] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
-  [161] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
-  [163] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 4, 0, 2),
-  [165] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 7, 0, 2),
-  [167] = {.entry = {.count = 1, .reusable = true}}, SHIFT(88),
-  [169] = {.entry = {.count = 1, .reusable = true}}, SHIFT(22),
-  [171] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 5, 0, 2),
-  [173] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
-  [175] = {.entry = {.count = 1, .reusable = true}}, SHIFT(71),
-  [177] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6),
-  [179] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
-  [181] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(71),
-  [184] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
-  [186] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
-  [188] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69),
-  [190] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0),
-  [192] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0),
-  [194] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 7, 0, 0),
-  [196] = {.entry = {.count = 1, .reusable = true}}, SHIFT(19),
-  [198] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60),
-  [200] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48),
-  [202] = {.entry = {.count = 1, .reusable = true}}, SHIFT(77),
-  [204] = {.entry = {.count = 1, .reusable = true}}, SHIFT(61),
-  [206] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
-  [208] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35),
-  [210] = {.entry = {.count = 1, .reusable = true}}, SHIFT(27),
-  [212] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12),
-  [214] = {.entry = {.count = 1, .reusable = true}}, SHIFT(47),
-  [216] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63),
-  [218] = {.entry = {.count = 1, .reusable = true}}, SHIFT(55),
-  [220] = {.entry = {.count = 1, .reusable = true}}, SHIFT(75),
-  [222] = {.entry = {.count = 1, .reusable = true}}, SHIFT(64),
-  [224] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
-  [226] = {.entry = {.count = 1, .reusable = true}}, SHIFT(41),
-  [228] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
-  [230] = {.entry = {.count = 1, .reusable = false}}, SHIFT(58),
-  [232] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49),
-  [234] = {.entry = {.count = 1, .reusable = true}}, SHIFT(76),
-  [236] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20),
-  [238] = {.entry = {.count = 1, .reusable = true}}, SHIFT(59),
-  [240] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
+  [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),
 };
 
 #ifdef __cplusplus
diff --git a/test/corpus/application.txt b/test/corpus/application.txt
index 58f1a58..adec6e8 100644
--- a/test/corpus/application.txt
+++ b/test/corpus/application.txt
@@ -17,7 +17,8 @@ def foo (A B : *) (f : A -> B) (x : A) :=
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (param_block
       (identifier)
       (expr
diff --git a/test/corpus/arrows.txt b/test/corpus/arrows.txt
index 88675c2..3daf5b7 100644
--- a/test/corpus/arrows.txt
+++ b/test/corpus/arrows.txt
@@ -16,7 +16,8 @@ def foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (param_block
       (identifier)
       (expr
diff --git a/test/corpus/axioms.txt b/test/corpus/axioms.txt
index 1b52a05..adce4fe 100644
--- a/test/corpus/axioms.txt
+++ b/test/corpus/axioms.txt
@@ -14,4 +14,5 @@ axiom nat : *;
         (app_term
           (app
             (term
-              (star))))))))
+              (sort
+                (star)))))))))
diff --git a/test/corpus/include.txt b/test/corpus/include.txt
index 4863ee1..d9cd8fa 100644
--- a/test/corpus/include.txt
+++ b/test/corpus/include.txt
@@ -21,7 +21,8 @@ def baz : * := A;
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (expr
       (app_term
         (app
diff --git a/test/corpus/labs.txt b/test/corpus/labs.txt
index a2ad2c1..707554a 100644
--- a/test/corpus/labs.txt
+++ b/test/corpus/labs.txt
@@ -18,7 +18,8 @@ def foo := fun (A : *) (x : A) : A => x;
               (app_term
                 (app
                   (term
-                    (star))))))
+                    (sort
+                      (star)))))))
           (param_block
             (identifier)
             (expr
diff --git a/test/corpus/pabs.txt b/test/corpus/pabs.txt
index 7d2f45c..2d16383 100644
--- a/test/corpus/pabs.txt
+++ b/test/corpus/pabs.txt
@@ -18,7 +18,8 @@ def rel := forall (A : *) (x : A), *;
               (app_term
                 (app
                   (term
-                    (star))))))
+                    (sort
+                      (star)))))))
           (param_block
             (identifier)
             (expr
@@ -30,4 +31,5 @@ def rel := forall (A : *) (x : A), *;
             (app_term
               (app
                 (term
-                  (star))))))))))
+                  (sort
+                    (star)))))))))))
diff --git a/test/corpus/params.txt b/test/corpus/params.txt
index 73b871c..62e45ea 100644
--- a/test/corpus/params.txt
+++ b/test/corpus/params.txt
@@ -15,7 +15,8 @@ def foo (A : *) (x y z : A) := x;
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (param_block
       (identifier)
       (identifier)