diff --git a/build.xml b/build.xml
index 780b405f..d3ebfead 100644
--- a/build.xml
+++ b/build.xml
@@ -3134,9 +3134,18 @@
+
+
+
+
+
+
+
+
+
diff --git a/coderules/solutions/jetbrains.mps.typechecking.build/models/jetbrains.mps.typechecking.build.mps b/coderules/solutions/jetbrains.mps.typechecking.build/models/jetbrains.mps.typechecking.build.mps
index 82d2f972..c8ce0397 100644
--- a/coderules/solutions/jetbrains.mps.typechecking.build/models/jetbrains.mps.typechecking.build.mps
+++ b/coderules/solutions/jetbrains.mps.typechecking.build/models/jetbrains.mps.typechecking.build.mps
@@ -931,6 +931,11 @@
+
+
+
+
+
diff --git a/coderules/solutions/jetbrains.mps.typechecking.test/models/jetbrains.mps.typechecking@tests.mps b/coderules/solutions/jetbrains.mps.typechecking.test/models/jetbrains.mps.typechecking@tests.mps
index 634a0b54..5c279d8c 100644
--- a/coderules/solutions/jetbrains.mps.typechecking.test/models/jetbrains.mps.typechecking@tests.mps
+++ b/coderules/solutions/jetbrains.mps.typechecking.test/models/jetbrains.mps.typechecking@tests.mps
@@ -1977,19 +1977,24 @@
-
-
+
+
-
+
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
-
@@ -2003,7 +2008,7 @@
-
+
@@ -2025,7 +2030,7 @@
-
+
diff --git a/coderules/solutions/jetbrains.mps.typechecking/jetbrains.mps.typechecking.msd b/coderules/solutions/jetbrains.mps.typechecking/jetbrains.mps.typechecking.msd
index 9f97cc1a..0f1e58b1 100644
--- a/coderules/solutions/jetbrains.mps.typechecking/jetbrains.mps.typechecking.msd
+++ b/coderules/solutions/jetbrains.mps.typechecking/jetbrains.mps.typechecking.msd
@@ -16,6 +16,7 @@
f97d84b2-8bad-4fdd-8ede-da17b3eacf4c(jetbrains.mps.coderules)
f486b8aa-5b2d-4ec0-8ef5-8f45d773fb84(jetbrains.mps.lang.typechecking.runtime)
0b80a2e8-f9f1-47b3-823f-56eb115bca42(jetbrains.mps.typechecking.annotation)
+ 7a5dda62-9140-4668-ab76-d5ed1746f2b2(jetbrains.mps.lang.typesystem)
@@ -45,11 +46,22 @@
+
+
+
+
+
+
+
+
+
+
+
diff --git a/coderules/solutions/jetbrains.mps.typechecking/models/service.mps b/coderules/solutions/jetbrains.mps.typechecking/models/service.mps
index e3e29ccd..0a405416 100644
--- a/coderules/solutions/jetbrains.mps.typechecking/models/service.mps
+++ b/coderules/solutions/jetbrains.mps.typechecking/models/service.mps
@@ -51,6 +51,7 @@
+
@@ -140,7 +141,6 @@
-
@@ -227,6 +227,7 @@
+
@@ -280,6 +281,9 @@
+
+
+
@@ -322,9 +326,6 @@
-
-
-
@@ -377,843 +378,982 @@
-
-
-
-
-
-
-
+
+
+
-
+
-
+
-
+
-
-
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
-
-
-
-
-
+
+
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
-
+
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
-
-
-
+
+
+
-
+
-
-
-
+
+
+
-
+
-
-
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
+
+
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps b/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps
index 3fb56577..669b3a6c 100644
--- a/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps
+++ b/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps
@@ -57,7 +57,6 @@
-
@@ -141,23 +140,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -166,23 +174,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -191,23 +208,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -216,23 +242,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
diff --git a/samples/fitch/solutions/samples.fitch.demo/models/herbrandLogic@tests.mps b/samples/fitch/solutions/samples.fitch.demo/models/herbrandLogic@tests.mps
index 49d1f67c..c428af03 100644
--- a/samples/fitch/solutions/samples.fitch.demo/models/herbrandLogic@tests.mps
+++ b/samples/fitch/solutions/samples.fitch.demo/models/herbrandLogic@tests.mps
@@ -57,7 +57,6 @@
-
@@ -138,23 +137,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
diff --git a/samples/fitch/solutions/samples.fitch.demo/models/propositionalLogic@tests.mps b/samples/fitch/solutions/samples.fitch.demo/models/propositionalLogic@tests.mps
index efecf958..8a42dda5 100644
--- a/samples/fitch/solutions/samples.fitch.demo/models/propositionalLogic@tests.mps
+++ b/samples/fitch/solutions/samples.fitch.demo/models/propositionalLogic@tests.mps
@@ -57,7 +57,6 @@
-
@@ -138,23 +137,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -163,23 +171,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -188,23 +205,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -213,23 +239,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -238,23 +273,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -263,23 +307,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -288,23 +341,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -313,23 +375,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -338,23 +409,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -363,23 +443,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -388,23 +477,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -413,23 +511,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
diff --git a/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps b/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps
index 7461e2dc..5d0bb414 100644
--- a/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps
+++ b/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps
@@ -57,7 +57,6 @@
-
@@ -141,23 +140,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -166,23 +174,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -191,22 +208,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
+
+
@@ -215,23 +242,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
@@ -240,23 +276,32 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+