From b4f3ae1ef62911d6bcd1ce366926dd409c8732d2 Mon Sep 17 00:00:00 2001
From: Fedor Isakov <fisakov@gmail.com>
Date: Wed, 15 Nov 2017 17:13:18 +0100
Subject: [PATCH] Introduce reiteration. Assumption to be used only as a
 subproof start.

---
 .../jetbrains.mps.fitch/models/behavior.mps   | 192 ++++++++++-
 .../models/constraints.mps                    |  35 ++
 .../jetbrains.mps.fitch/models/editor.mps     | 314 +++++++++++++++++-
 .../jetbrains.mps.fitch/models/structure.mps  |   8 +
 .../jetbrains.mps.fitch/models/types.mps      | 186 +++++++++++
 .../models/jetbrains.mps.fitch.sandbox.mps    |  41 ++-
 6 files changed, 753 insertions(+), 23 deletions(-)

diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps
index f0bca7ae..7d640b98 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps
@@ -8,6 +8,196 @@
   <imports>
     <import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
   </imports>
-  <registry />
+  <registry>
+    <language id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior">
+      <concept id="1225194240794" name="jetbrains.mps.lang.behavior.structure.ConceptBehavior" flags="ng" index="13h7C7">
+        <reference id="1225194240799" name="concept" index="13h7C2" />
+        <child id="1225194240805" name="method" index="13h7CS" />
+        <child id="1225194240801" name="constructor" index="13h7CW" />
+      </concept>
+      <concept id="1225194413805" name="jetbrains.mps.lang.behavior.structure.ConceptConstructorDeclaration" flags="in" index="13hLZK" />
+      <concept id="1225194472830" name="jetbrains.mps.lang.behavior.structure.ConceptMethodDeclaration" flags="ng" index="13i0hz">
+        <property id="1225194472832" name="isVirtual" index="13i0it" />
+        <property id="1225194472834" name="isAbstract" index="13i0iv" />
+      </concept>
+      <concept id="1225194691553" name="jetbrains.mps.lang.behavior.structure.ThisNodeExpression" flags="nn" index="13iPFW" />
+    </language>
+    <language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
+      <concept id="1197027756228" name="jetbrains.mps.baseLanguage.structure.DotExpression" flags="nn" index="2OqwBi">
+        <child id="1197027771414" name="operand" index="2Oq$k0" />
+        <child id="1197027833540" name="operation" index="2OqNvi" />
+      </concept>
+      <concept id="1145552977093" name="jetbrains.mps.baseLanguage.structure.GenericNewExpression" flags="nn" index="2ShNRf">
+        <child id="1145553007750" name="creator" index="2ShVmc" />
+      </concept>
+      <concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
+        <child id="1137022507850" name="body" index="2VODD2" />
+      </concept>
+      <concept id="1068431474542" name="jetbrains.mps.baseLanguage.structure.VariableDeclaration" flags="ng" index="33uBYm">
+        <child id="1068431790190" name="initializer" index="33vP2m" />
+      </concept>
+      <concept id="1068498886296" name="jetbrains.mps.baseLanguage.structure.VariableReference" flags="nn" index="37vLTw">
+        <reference id="1068581517664" name="variableDeclaration" index="3cqZAo" />
+      </concept>
+      <concept id="4972933694980447171" name="jetbrains.mps.baseLanguage.structure.BaseVariableDeclaration" flags="ng" index="19Szcq">
+        <child id="5680397130376446158" name="type" index="1tU5fm" />
+      </concept>
+      <concept id="1068580123132" name="jetbrains.mps.baseLanguage.structure.BaseMethodDeclaration" flags="ng" index="3clF44">
+        <child id="1068580123133" name="returnType" index="3clF45" />
+        <child id="1068580123135" name="body" index="3clF47" />
+      </concept>
+      <concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
+        <child id="1068580123156" name="expression" index="3clFbG" />
+      </concept>
+      <concept id="1068580123159" name="jetbrains.mps.baseLanguage.structure.IfStatement" flags="nn" index="3clFbJ">
+        <child id="1068580123160" name="condition" index="3clFbw" />
+        <child id="1068580123161" name="ifTrue" index="3clFbx" />
+      </concept>
+      <concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
+        <child id="1068581517665" name="statement" index="3cqZAp" />
+      </concept>
+      <concept id="1068581242864" name="jetbrains.mps.baseLanguage.structure.LocalVariableDeclarationStatement" flags="nn" index="3cpWs8">
+        <child id="1068581242865" name="localVariableDeclaration" index="3cpWs9" />
+      </concept>
+      <concept id="1068581242863" name="jetbrains.mps.baseLanguage.structure.LocalVariableDeclaration" flags="nr" index="3cpWsn" />
+      <concept id="1204053956946" name="jetbrains.mps.baseLanguage.structure.IMethodCall" flags="ng" index="1ndlxa">
+        <reference id="1068499141037" name="baseMethodDeclaration" index="37wK5l" />
+      </concept>
+      <concept id="1178549954367" name="jetbrains.mps.baseLanguage.structure.IVisible" flags="ng" index="1B3ioH">
+        <child id="1178549979242" name="visibility" index="1B3o_S" />
+      </concept>
+      <concept id="1146644602865" name="jetbrains.mps.baseLanguage.structure.PublicVisibility" flags="nn" index="3Tm1VV" />
+    </language>
+    <language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
+      <concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
+        <reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
+      </concept>
+      <concept id="1138411891628" name="jetbrains.mps.lang.smodel.structure.SNodeOperation" flags="nn" index="eCIE_">
+        <child id="1144104376918" name="parameter" index="1xVPHs" />
+      </concept>
+      <concept id="1179409122411" name="jetbrains.mps.lang.smodel.structure.Node_ConceptMethodCall" flags="nn" index="2qgKlT" />
+      <concept id="2396822768958367367" name="jetbrains.mps.lang.smodel.structure.AbstractTypeCastExpression" flags="nn" index="$5XWr">
+        <child id="6733348108486823193" name="leftExpression" index="1m5AlR" />
+        <child id="3906496115198199033" name="conceptArgument" index="3oSUPX" />
+      </concept>
+      <concept id="1145383075378" name="jetbrains.mps.lang.smodel.structure.SNodeListType" flags="in" index="2I9FWS">
+        <reference id="1145383142433" name="elementConcept" index="2I9WkF" />
+      </concept>
+      <concept id="1145567426890" name="jetbrains.mps.lang.smodel.structure.SNodeListCreator" flags="nn" index="2T8Vx0">
+        <child id="1145567471833" name="createdType" index="2T96Bj" />
+      </concept>
+      <concept id="1145572800087" name="jetbrains.mps.lang.smodel.structure.Node_GetPrevSiblingsOperation" flags="nn" index="2Ttrtt" />
+      <concept id="1139613262185" name="jetbrains.mps.lang.smodel.structure.Node_GetParentOperation" flags="nn" index="1mfA1w" />
+      <concept id="1139621453865" name="jetbrains.mps.lang.smodel.structure.Node_IsInstanceOfOperation" flags="nn" index="1mIQ4w">
+        <child id="1177027386292" name="conceptArgument" index="cj9EA" />
+      </concept>
+      <concept id="1144100932627" name="jetbrains.mps.lang.smodel.structure.OperationParm_Inclusion" flags="ng" index="1xIGOp" />
+      <concept id="1140137987495" name="jetbrains.mps.lang.smodel.structure.SNodeTypeCastExpression" flags="nn" index="1PxgMI">
+        <property id="1238684351431" name="asCast" index="1BlNFB" />
+      </concept>
+    </language>
+    <language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
+      <concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
+        <property id="1193676396447" name="virtualPackage" index="3GE5qa" />
+      </concept>
+      <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
+        <property id="1169194664001" name="name" index="TrG5h" />
+      </concept>
+    </language>
+    <language id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections">
+      <concept id="540871147943773365" name="jetbrains.mps.baseLanguage.collections.structure.SingleArgumentSequenceOperation" flags="nn" index="25WWJ4">
+        <child id="540871147943773366" name="argument" index="25WWJ7" />
+      </concept>
+      <concept id="1160666733551" name="jetbrains.mps.baseLanguage.collections.structure.AddAllElementsOperation" flags="nn" index="X8dFx" />
+    </language>
+  </registry>
+  <node concept="13h7C7" id="5jVx7S20nJq">
+    <property role="3GE5qa" value="proof" />
+    <ref role="13h7C2" to="jfgh:3JXBM6C3UQB" resolve="Node" />
+    <node concept="13i0hz" id="5jVx7S20nJ_" role="13h7CS">
+      <property role="13i0iv" value="false" />
+      <property role="13i0it" value="true" />
+      <property role="TrG5h" value="allInScope" />
+      <node concept="3Tm1VV" id="5jVx7S20nJA" role="1B3o_S" />
+      <node concept="2I9FWS" id="5jVx7S20nJX" role="3clF45" />
+      <node concept="3clFbS" id="5jVx7S20nJC" role="3clF47">
+        <node concept="3cpWs8" id="5jVx7S20pHO" role="3cqZAp">
+          <node concept="3cpWsn" id="5jVx7S20pHP" role="3cpWs9">
+            <property role="TrG5h" value="res" />
+            <node concept="2I9FWS" id="5jVx7S20pHM" role="1tU5fm" />
+            <node concept="2ShNRf" id="5jVx7S20pHQ" role="33vP2m">
+              <node concept="2T8Vx0" id="5jVx7S20pHR" role="2ShVmc">
+                <node concept="2I9FWS" id="5jVx7S20pHS" role="2T96Bj">
+                  <ref role="2I9WkF" to="jfgh:3JXBM6C3UQB" resolve="Node" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="3clFbF" id="5jVx7S20p4M" role="3cqZAp">
+          <node concept="2OqwBi" id="5jVx7S20r7R" role="3clFbG">
+            <node concept="37vLTw" id="5jVx7S20pHT" role="2Oq$k0">
+              <ref role="3cqZAo" node="5jVx7S20pHP" resolve="res" />
+            </node>
+            <node concept="X8dFx" id="5jVx7S20u1s" role="2OqNvi">
+              <node concept="2OqwBi" id="5jVx7S20ukK" role="25WWJ7">
+                <node concept="13iPFW" id="5jVx7S20ukL" role="2Oq$k0" />
+                <node concept="2Ttrtt" id="5jVx7S20ukM" role="2OqNvi">
+                  <node concept="1xIGOp" id="5jVx7S20ukN" role="1xVPHs" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="3clFbJ" id="5jVx7S20x$s" role="3cqZAp">
+          <node concept="3clFbS" id="5jVx7S20x$u" role="3clFbx">
+            <node concept="3clFbF" id="5jVx7S20yHF" role="3cqZAp">
+              <node concept="2OqwBi" id="5jVx7S20zzA" role="3clFbG">
+                <node concept="37vLTw" id="5jVx7S20yHD" role="2Oq$k0">
+                  <ref role="3cqZAo" node="5jVx7S20pHP" resolve="res" />
+                </node>
+                <node concept="X8dFx" id="5jVx7S20_KG" role="2OqNvi">
+                  <node concept="2OqwBi" id="5jVx7S20Den" role="25WWJ7">
+                    <node concept="1PxgMI" id="5jVx7S20C$P" role="2Oq$k0">
+                      <property role="1BlNFB" value="true" />
+                      <node concept="chp4Y" id="5jVx7S20CFC" role="3oSUPX">
+                        <ref role="cht4Q" to="jfgh:3JXBM6C3UQB" resolve="Node" />
+                      </node>
+                      <node concept="2OqwBi" id="5jVx7S20Abu" role="1m5AlR">
+                        <node concept="13iPFW" id="5jVx7S20_Y8" role="2Oq$k0" />
+                        <node concept="1mfA1w" id="5jVx7S20Bs0" role="2OqNvi" />
+                      </node>
+                    </node>
+                    <node concept="2qgKlT" id="5jVx7S20EVk" role="2OqNvi">
+                      <ref role="37wK5l" node="5jVx7S20nJ_" resolve="allInScope" />
+                    </node>
+                  </node>
+                </node>
+              </node>
+            </node>
+          </node>
+          <node concept="2OqwBi" id="5jVx7S20ypd" role="3clFbw">
+            <node concept="2OqwBi" id="5jVx7S20xPu" role="2Oq$k0">
+              <node concept="13iPFW" id="5jVx7S20xH1" role="2Oq$k0" />
+              <node concept="1mfA1w" id="5jVx7S20xYY" role="2OqNvi" />
+            </node>
+            <node concept="1mIQ4w" id="5jVx7S20yDs" role="2OqNvi">
+              <node concept="chp4Y" id="5jVx7S20yFx" role="cj9EA">
+                <ref role="cht4Q" to="jfgh:3JXBM6C3UQB" resolve="Node" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="3clFbF" id="5jVx7S20Frf" role="3cqZAp">
+          <node concept="37vLTw" id="5jVx7S20Frd" role="3clFbG">
+            <ref role="3cqZAo" node="5jVx7S20pHP" resolve="res" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="13hLZK" id="5jVx7S20nJr" role="13h7CW">
+      <node concept="3clFbS" id="5jVx7S20nJs" role="2VODD2" />
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/constraints.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/constraints.mps
index 708ccad7..6c835006 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/constraints.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/constraints.mps
@@ -32,6 +32,7 @@
       <concept id="4972933694980447171" name="jetbrains.mps.baseLanguage.structure.BaseVariableDeclaration" flags="ng" index="19Szcq">
         <child id="5680397130376446158" name="type" index="1tU5fm" />
       </concept>
+      <concept id="1068580123152" name="jetbrains.mps.baseLanguage.structure.EqualsExpression" flags="nn" index="3clFbC" />
       <concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
         <child id="1068580123156" name="expression" index="3clFbG" />
       </concept>
@@ -61,8 +62,11 @@
         <child id="1163668922816" name="ifTrue" index="3K4E3e" />
         <child id="1163668934364" name="ifFalse" index="3K4GZi" />
       </concept>
+      <concept id="1080120340718" name="jetbrains.mps.baseLanguage.structure.AndExpression" flags="nn" index="1Wc70l" />
     </language>
     <language id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints">
+      <concept id="6702802731807351367" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAChild" flags="in" index="9S07l" />
+      <concept id="1202989658459" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_parentNode" flags="nn" index="nLn13" />
       <concept id="1147467115080" name="jetbrains.mps.lang.constraints.structure.NodePropertyConstraint" flags="ng" index="EnEH3">
         <reference id="1147467295099" name="applicableProperty" index="EomxK" />
         <child id="1147468630220" name="propertyGetter" index="EtsB7" />
@@ -73,6 +77,7 @@
       <concept id="1212096972063" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_PropertyValidator" flags="in" index="QB0g5" />
       <concept id="1213093968558" name="jetbrains.mps.lang.constraints.structure.ConceptConstraints" flags="ng" index="1M2fIO">
         <reference id="1213093996982" name="concept" index="1M2myG" />
+        <child id="6702802731807737306" name="canBeChild" index="9Vyp8" />
         <child id="1213098023997" name="property" index="1MhHOB" />
       </concept>
       <concept id="1153138554286" name="jetbrains.mps.lang.constraints.structure.ConstraintsFunctionParameter_propertyValue" flags="nn" index="1Wqviy" />
@@ -84,6 +89,7 @@
       </concept>
     </language>
     <language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
+      <concept id="1179168000618" name="jetbrains.mps.lang.smodel.structure.Node_GetIndexInParentOperation" flags="nn" index="2bSWHS" />
       <concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
         <reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
       </concept>
@@ -397,5 +403,34 @@
       </node>
     </node>
   </node>
+  <node concept="1M2fIO" id="5jVx7S22QGW">
+    <property role="3GE5qa" value="proof.reasoning" />
+    <ref role="1M2myG" to="jfgh:3JXBM6C3Pwi" resolve="Assumption" />
+    <node concept="9S07l" id="5jVx7S22QGX" role="9Vyp8">
+      <node concept="3clFbS" id="5jVx7S22QGY" role="2VODD2">
+        <node concept="3clFbF" id="5jVx7S22QO7" role="3cqZAp">
+          <node concept="1Wc70l" id="5jVx7S22S$w" role="3clFbG">
+            <node concept="3clFbC" id="5jVx7S22VSB" role="3uHU7w">
+              <node concept="3cmrfG" id="5jVx7S22Wl1" role="3uHU7w">
+                <property role="3cmrfH" value="0" />
+              </node>
+              <node concept="2OqwBi" id="5jVx7S22T0M" role="3uHU7B">
+                <node concept="EsrRn" id="5jVx7S22SJQ" role="2Oq$k0" />
+                <node concept="2bSWHS" id="5jVx7S22Tz3" role="2OqNvi" />
+              </node>
+            </node>
+            <node concept="2OqwBi" id="5jVx7S22R3d" role="3uHU7B">
+              <node concept="nLn13" id="5jVx7S22QO6" role="2Oq$k0" />
+              <node concept="1mIQ4w" id="5jVx7S22Rfk" role="2OqNvi">
+                <node concept="chp4Y" id="5jVx7S22RrK" role="cj9EA">
+                  <ref role="cht4Q" to="jfgh:3JXBM6C3UQ$" resolve="SubProof" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/editor.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/editor.mps
index ff2ee350..8f2e4e4d 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/editor.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/editor.mps
@@ -13,6 +13,7 @@
     <import index="wyt6" ref="6354ebe7-c22a-4a0f-ac54-50b52ab9b065/java:java.lang(JDK/)" implicit="true" />
     <import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" implicit="true" />
     <import index="tpco" ref="r:00000000-0000-4000-0000-011c89590284(jetbrains.mps.lang.core.editor)" implicit="true" />
+    <import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" implicit="true" />
   </imports>
   <registry>
     <language id="18bc6592-03a6-4e29-a83a-7ff23bde13ba" name="jetbrains.mps.lang.editor">
@@ -59,6 +60,7 @@
       <concept id="8329266386016608055" name="jetbrains.mps.lang.editor.structure.ApproveDelete_Operation" flags="ng" index="2xy62i">
         <child id="8329266386016685951" name="editorContext" index="2xHN3q" />
       </concept>
+      <concept id="8371900013785948369" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_Parameter" flags="ig" index="2$S_p_" />
       <concept id="5944657839000868711" name="jetbrains.mps.lang.editor.structure.ConceptEditorContextHints" flags="ig" index="2ABfQD">
         <child id="5944657839000877563" name="hints" index="2ABdcP" />
       </concept>
@@ -68,6 +70,10 @@
       <concept id="3473224453637651916" name="jetbrains.mps.lang.editor.structure.TransformationLocation_SideTransform_PlaceInCellHolder" flags="ng" index="CtIbL">
         <property id="3473224453637651917" name="placeInCell" index="CtIbK" />
       </concept>
+      <concept id="308059530142752797" name="jetbrains.mps.lang.editor.structure.SubstituteMenuPart_Parameterized" flags="ng" index="2F$Pav">
+        <child id="8371900013785948359" name="part" index="2$S_pN" />
+        <child id="8371900013785948365" name="parameterQuery" index="2$S_pT" />
+      </concept>
       <concept id="1638911550608571617" name="jetbrains.mps.lang.editor.structure.TransformationMenu_Default" flags="ng" index="IW6AY" />
       <concept id="1638911550608610798" name="jetbrains.mps.lang.editor.structure.QueryFunction_TransformationMenu_Execute" flags="ig" index="IWg2L" />
       <concept id="1638911550608610278" name="jetbrains.mps.lang.editor.structure.TransformationMenuPart_Action" flags="ng" index="IWgqT">
@@ -81,10 +87,15 @@
       <concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
         <property id="1186414551515" name="flag" index="VOm3f" />
       </concept>
+      <concept id="1186414860679" name="jetbrains.mps.lang.editor.structure.EditableStyleClassItem" flags="ln" index="VPxyj" />
       <concept id="1186414928363" name="jetbrains.mps.lang.editor.structure.SelectableStyleSheetItem" flags="ln" index="VPM3Z" />
       <concept id="1630016958697344083" name="jetbrains.mps.lang.editor.structure.IMenu_Concept" flags="ng" index="2ZABuq">
         <reference id="6591946374543067572" name="conceptDeclaration" index="aqKnT" />
       </concept>
+      <concept id="1630016958697286851" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_parameterObject" flags="ng" index="2ZBlsa" />
+      <concept id="1630016958697057551" name="jetbrains.mps.lang.editor.structure.IMenuPartParameterized" flags="ng" index="2ZBHr6">
+        <child id="1630016958697057552" name="parameterType" index="2ZBHrp" />
+      </concept>
       <concept id="1233758997495" name="jetbrains.mps.lang.editor.structure.PunctuationLeftStyleClassItem" flags="ln" index="11L4FC" />
       <concept id="1233759184865" name="jetbrains.mps.lang.editor.structure.PunctuationRightStyleClassItem" flags="ln" index="11LMrY" />
       <concept id="8998492695583125082" name="jetbrains.mps.lang.editor.structure.SubstituteFeature_MatchingText" flags="ng" index="16NfWO">
@@ -93,6 +104,7 @@
       <concept id="8998492695583129971" name="jetbrains.mps.lang.editor.structure.SubstituteFeature_DescriptionText" flags="ng" index="16NL0t">
         <child id="8998492695583129972" name="query" index="16NL0q" />
       </concept>
+      <concept id="1154465273778" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_SubstituteMenu_ParentNode" flags="nn" index="3bvxqY" />
       <concept id="2896773699153795590" name="jetbrains.mps.lang.editor.structure.TransformationLocation_SideTransform" flags="ng" index="3cWJ9i">
         <child id="3473224453637651919" name="placeInCell" index="CtIbM" />
       </concept>
@@ -158,6 +170,7 @@
         <child id="7980428675268276159" name="parts" index="1Qtc8A" />
       </concept>
       <concept id="1176717841777" name="jetbrains.mps.lang.editor.structure.QueryFunction_ModelAccess_Getter" flags="in" index="3TQlhw" />
+      <concept id="2722384699544370949" name="jetbrains.mps.lang.editor.structure.SubstituteMenuPart_Placeholder" flags="ng" index="3VyMlK" />
       <concept id="4307758654696938365" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_RefPresentation" flags="ig" index="1WAQ3h" />
       <concept id="4307758654696952957" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_SubstituteMenu_ReferencedNode" flags="ng" index="1WAUZh" />
       <concept id="8428109087107030357" name="jetbrains.mps.lang.editor.structure.SubstituteMenuPart_ReferenceScope" flags="ng" index="3XHNnq">
@@ -169,6 +182,8 @@
       </concept>
     </language>
     <language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
+      <concept id="1080223426719" name="jetbrains.mps.baseLanguage.structure.OrExpression" flags="nn" index="22lmx$" />
+      <concept id="4836112446988635817" name="jetbrains.mps.baseLanguage.structure.UndefinedType" flags="in" index="2jxLKc" />
       <concept id="1197027756228" name="jetbrains.mps.baseLanguage.structure.DotExpression" flags="nn" index="2OqwBi">
         <child id="1197027771414" name="operand" index="2Oq$k0" />
         <child id="1197027833540" name="operation" index="2OqNvi" />
@@ -185,12 +200,14 @@
       <concept id="1081236700937" name="jetbrains.mps.baseLanguage.structure.StaticMethodCall" flags="nn" index="2YIFZM">
         <reference id="1144433194310" name="classConcept" index="1Pybhc" />
       </concept>
+      <concept id="1070534058343" name="jetbrains.mps.baseLanguage.structure.NullLiteral" flags="nn" index="10Nm6u" />
       <concept id="1068431474542" name="jetbrains.mps.baseLanguage.structure.VariableDeclaration" flags="ng" index="33uBYm">
         <child id="1068431790190" name="initializer" index="33vP2m" />
       </concept>
       <concept id="1068498886296" name="jetbrains.mps.baseLanguage.structure.VariableReference" flags="nn" index="37vLTw">
         <reference id="1068581517664" name="variableDeclaration" index="3cqZAo" />
       </concept>
+      <concept id="1068498886292" name="jetbrains.mps.baseLanguage.structure.ParameterDeclaration" flags="ir" index="37vLTG" />
       <concept id="4972933694980447171" name="jetbrains.mps.baseLanguage.structure.BaseVariableDeclaration" flags="ng" index="19Szcq">
         <child id="5680397130376446158" name="type" index="1tU5fm" />
       </concept>
@@ -198,12 +215,17 @@
       <concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
         <child id="1068580123156" name="expression" index="3clFbG" />
       </concept>
+      <concept id="1068580123159" name="jetbrains.mps.baseLanguage.structure.IfStatement" flags="nn" index="3clFbJ">
+        <child id="1068580123160" name="condition" index="3clFbw" />
+        <child id="1068580123161" name="ifTrue" index="3clFbx" />
+      </concept>
       <concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
         <child id="1068581517665" name="statement" index="3cqZAp" />
       </concept>
       <concept id="1068580320020" name="jetbrains.mps.baseLanguage.structure.IntegerConstant" flags="nn" index="3cmrfG">
         <property id="1068580320021" name="value" index="3cmrfH" />
       </concept>
+      <concept id="1068581242875" name="jetbrains.mps.baseLanguage.structure.PlusExpression" flags="nn" index="3cpWs3" />
       <concept id="1068581242878" name="jetbrains.mps.baseLanguage.structure.ReturnStatement" flags="nn" index="3cpWs6">
         <child id="1068581517676" name="expression" index="3cqZAk" />
       </concept>
@@ -220,26 +242,53 @@
         <child id="1081773367580" name="leftExpression" index="3uHU7B" />
       </concept>
     </language>
+    <language id="fd392034-7849-419d-9071-12563d152375" name="jetbrains.mps.baseLanguage.closures">
+      <concept id="1199569711397" name="jetbrains.mps.baseLanguage.closures.structure.ClosureLiteral" flags="nn" index="1bVj0M">
+        <child id="1199569906740" name="parameter" index="1bW2Oz" />
+        <child id="1199569916463" name="body" index="1bW5cS" />
+      </concept>
+    </language>
     <language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
+      <concept id="1177026924588" name="jetbrains.mps.lang.smodel.structure.RefConcept_Reference" flags="nn" index="chp4Y">
+        <reference id="1177026940964" name="conceptDeclaration" index="cht4Q" />
+      </concept>
       <concept id="1140725362528" name="jetbrains.mps.lang.smodel.structure.Link_SetTargetOperation" flags="nn" index="2oxUTD">
         <child id="1140725362529" name="linkTarget" index="2oxUTC" />
       </concept>
+      <concept id="1179409122411" name="jetbrains.mps.lang.smodel.structure.Node_ConceptMethodCall" flags="nn" index="2qgKlT" />
       <concept id="1138661924179" name="jetbrains.mps.lang.smodel.structure.Property_SetOperation" flags="nn" index="tyxLq">
         <child id="1138662048170" name="value" index="tz02z" />
       </concept>
       <concept id="1138757581985" name="jetbrains.mps.lang.smodel.structure.Link_SetNewChildOperation" flags="nn" index="zfrQC" />
+      <concept id="2396822768958367367" name="jetbrains.mps.lang.smodel.structure.AbstractTypeCastExpression" flags="nn" index="$5XWr">
+        <child id="6733348108486823193" name="leftExpression" index="1m5AlR" />
+        <child id="3906496115198199033" name="conceptArgument" index="3oSUPX" />
+      </concept>
+      <concept id="1145383075378" name="jetbrains.mps.lang.smodel.structure.SNodeListType" flags="in" index="2I9FWS">
+        <reference id="1145383142433" name="elementConcept" index="2I9WkF" />
+      </concept>
+      <concept id="1145567426890" name="jetbrains.mps.lang.smodel.structure.SNodeListCreator" flags="nn" index="2T8Vx0">
+        <child id="1145567471833" name="createdType" index="2T96Bj" />
+      </concept>
       <concept id="1139184414036" name="jetbrains.mps.lang.smodel.structure.LinkList_AddNewChildOperation" flags="nn" index="WFELt">
         <reference id="1139877738879" name="concept" index="1A0vxQ" />
       </concept>
+      <concept id="1139621453865" name="jetbrains.mps.lang.smodel.structure.Node_IsInstanceOfOperation" flags="nn" index="1mIQ4w">
+        <child id="1177027386292" name="conceptArgument" index="cj9EA" />
+      </concept>
       <concept id="1180636770613" name="jetbrains.mps.lang.smodel.structure.SNodeCreator" flags="nn" index="3zrR0B">
         <child id="1180636770616" name="createdType" index="3zrR0E" />
       </concept>
+      <concept id="1144146199828" name="jetbrains.mps.lang.smodel.structure.Node_CopyOperation" flags="nn" index="1$rogu" />
       <concept id="1139867745658" name="jetbrains.mps.lang.smodel.structure.Node_ReplaceWithNewOperation" flags="nn" index="1_qnLN">
         <reference id="1139867957129" name="concept" index="1_rbq0" />
       </concept>
       <concept id="1140131837776" name="jetbrains.mps.lang.smodel.structure.Node_ReplaceWithAnotherOperation" flags="nn" index="1P9Npp">
         <child id="1140131861877" name="replacementNode" index="1P9ThW" />
       </concept>
+      <concept id="1140137987495" name="jetbrains.mps.lang.smodel.structure.SNodeTypeCastExpression" flags="nn" index="1PxgMI">
+        <property id="1238684351431" name="asCast" index="1BlNFB" />
+      </concept>
       <concept id="1138055754698" name="jetbrains.mps.lang.smodel.structure.SNodeType" flags="in" index="3Tqbb2">
         <reference id="1138405853777" name="concept" index="ehGHo" />
       </concept>
@@ -282,12 +331,21 @@
       </concept>
     </language>
     <language id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections">
+      <concept id="1204796164442" name="jetbrains.mps.baseLanguage.collections.structure.InternalSequenceOperation" flags="nn" index="23sCx2">
+        <child id="1204796294226" name="closure" index="23t8la" />
+      </concept>
       <concept id="540871147943773365" name="jetbrains.mps.baseLanguage.collections.structure.SingleArgumentSequenceOperation" flags="nn" index="25WWJ4">
         <child id="540871147943773366" name="argument" index="25WWJ7" />
       </concept>
+      <concept id="1151702311717" name="jetbrains.mps.baseLanguage.collections.structure.ToListOperation" flags="nn" index="ANE8D" />
+      <concept id="1203518072036" name="jetbrains.mps.baseLanguage.collections.structure.SmartClosureParameterDeclaration" flags="ig" index="Rh6nW" />
       <concept id="1160612413312" name="jetbrains.mps.baseLanguage.collections.structure.AddElementOperation" flags="nn" index="TSZUe" />
       <concept id="1162935959151" name="jetbrains.mps.baseLanguage.collections.structure.GetSizeOperation" flags="nn" index="34oBXx" />
       <concept id="1165525191778" name="jetbrains.mps.baseLanguage.collections.structure.GetFirstOperation" flags="nn" index="1uHKPH" />
+      <concept id="1202120902084" name="jetbrains.mps.baseLanguage.collections.structure.WhereOperation" flags="nn" index="3zZkjj" />
+      <concept id="1522217801069396578" name="jetbrains.mps.baseLanguage.collections.structure.FoldLeftOperation" flags="nn" index="1MD8d$">
+        <child id="1522217801069421796" name="seed" index="1MDeny" />
+      </concept>
     </language>
   </registry>
   <node concept="24kQdi" id="3JXBM6C3Cnb">
@@ -1716,7 +1774,7 @@
     <node concept="3EZMnI" id="5RfK0kxjn86" role="2wV5jI">
       <node concept="l2Vlx" id="5RfK0kxjn87" role="2iSdaV" />
       <node concept="3F0ifn" id="5RfK0kxjSf2" role="3EZMnx">
-        <property role="3F0ifm" value="(Assumption)" />
+        <property role="3F0ifm" value="(A)" />
         <node concept="Vb9p2" id="5RfK0kxjSf4" role="3F10Kt" />
       </node>
     </node>
@@ -1730,7 +1788,7 @@
     <node concept="3EZMnI" id="$u9BK_zHtD" role="2wV5jI">
       <node concept="3F0ifn" id="$u9BK_zTQU" role="3EZMnx">
         <property role="3F0ifm" value="(" />
-        <node concept="VPM3Z" id="$u9BK_$dvp" role="3F10Kt">
+        <node concept="VPxyj" id="5jVx7S21EvR" role="3F10Kt">
           <property role="VOm3f" value="false" />
         </node>
         <node concept="11LMrY" id="$u9BK_zTRj" role="3F10Kt">
@@ -1740,14 +1798,14 @@
       </node>
       <node concept="PMmxH" id="$u9BK_zHtM" role="3EZMnx">
         <ref role="PMmxG" to="tpco:2wZex4PafBj" resolve="alias" />
-        <node concept="VPM3Z" id="$u9BK_$dvv" role="3F10Kt">
+        <node concept="VPxyj" id="5jVx7S21Ew0" role="3F10Kt">
           <property role="VOm3f" value="false" />
         </node>
         <node concept="Vb9p2" id="5RfK0kxkpvl" role="3F10Kt" />
       </node>
       <node concept="3F0ifn" id="$u9BK_zTRa" role="3EZMnx">
         <property role="3F0ifm" value=")" />
-        <node concept="VPM3Z" id="$u9BK_$dv_" role="3F10Kt">
+        <node concept="VPxyj" id="5jVx7S21Ewa" role="3F10Kt">
           <property role="VOm3f" value="false" />
         </node>
         <node concept="11L4FC" id="$u9BK_zTRl" role="3F10Kt">
@@ -1792,7 +1850,7 @@
     <node concept="3EZMnI" id="5RfK0kxjn8e" role="2wV5jI">
       <node concept="l2Vlx" id="5RfK0kxjn8f" role="2iSdaV" />
       <node concept="3F0ifn" id="5RfK0kxjFjS" role="3EZMnx">
-        <property role="3F0ifm" value="(Premise)" />
+        <property role="3F0ifm" value="(P)" />
         <node concept="Vb9p2" id="5RfK0kxjFjU" role="3F10Kt" />
       </node>
     </node>
@@ -1849,5 +1907,251 @@
       <property role="3F0ifm" value="OK" />
     </node>
   </node>
+  <node concept="3p36aQ" id="5jVx7S1YuHD">
+    <property role="3GE5qa" value="proof.reasoning" />
+    <ref role="aqKnT" to="jfgh:5jVx7S1Yau5" resolve="Reiteration" />
+    <node concept="2F$Pav" id="5jVx7S1YuHE" role="3ft7WO">
+      <node concept="3eGOop" id="5jVx7S1ZzTI" role="2$S_pN">
+        <node concept="ucgPf" id="5jVx7S1ZzTK" role="3aKz83">
+          <node concept="3clFbS" id="5jVx7S1ZzTM" role="2VODD2">
+            <node concept="3cpWs8" id="5jVx7S1Z$Hx" role="3cqZAp">
+              <node concept="3cpWsn" id="5jVx7S1Z$Hy" role="3cpWs9">
+                <property role="TrG5h" value="reit" />
+                <node concept="3Tqbb2" id="5jVx7S1Z$Hw" role="1tU5fm">
+                  <ref role="ehGHo" to="jfgh:5jVx7S1Yau5" resolve="Reiteration" />
+                </node>
+                <node concept="2ShNRf" id="5jVx7S1Z$Hz" role="33vP2m">
+                  <node concept="3zrR0B" id="5jVx7S1Z$H$" role="2ShVmc">
+                    <node concept="3Tqbb2" id="5jVx7S1Z$H_" role="3zrR0E">
+                      <ref role="ehGHo" to="jfgh:5jVx7S1Yau5" resolve="Reiteration" />
+                    </node>
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3cpWs8" id="5jVx7S1ZHTo" role="3cqZAp">
+              <node concept="3cpWsn" id="5jVx7S1ZHTp" role="3cpWs9">
+                <property role="TrG5h" value="b" />
+                <node concept="3Tqbb2" id="5jVx7S1ZHTn" role="1tU5fm">
+                  <ref role="ehGHo" to="jfgh:3JXBM6C3FsN" resolve="Basis" />
+                </node>
+                <node concept="2OqwBi" id="5jVx7S1ZHTq" role="33vP2m">
+                  <node concept="2OqwBi" id="5jVx7S1ZHTr" role="2Oq$k0">
+                    <node concept="37vLTw" id="5jVx7S1ZHTs" role="2Oq$k0">
+                      <ref role="3cqZAo" node="5jVx7S1Z$Hy" resolve="reit" />
+                    </node>
+                    <node concept="3Tsc0h" id="5jVx7S1ZHTt" role="2OqNvi">
+                      <ref role="3TtcxE" to="jfgh:3JXBM6C3MQ0" resolve="premise" />
+                    </node>
+                  </node>
+                  <node concept="WFELt" id="5jVx7S1ZHTu" role="2OqNvi" />
+                </node>
+              </node>
+            </node>
+            <node concept="3clFbF" id="5jVx7S1Z$mZ" role="3cqZAp">
+              <node concept="2OqwBi" id="5jVx7S1ZIYw" role="3clFbG">
+                <node concept="2OqwBi" id="5jVx7S1ZImq" role="2Oq$k0">
+                  <node concept="37vLTw" id="5jVx7S1ZHTv" role="2Oq$k0">
+                    <ref role="3cqZAo" node="5jVx7S1ZHTp" resolve="b" />
+                  </node>
+                  <node concept="3TrEf2" id="5jVx7S1ZI$B" role="2OqNvi">
+                    <ref role="3Tt5mk" to="jfgh:3JXBM6C3FuH" resolve="reasoning" />
+                  </node>
+                </node>
+                <node concept="2oxUTD" id="5jVx7S1ZJj2" role="2OqNvi">
+                  <node concept="2ZBlsa" id="5jVx7S1ZJOx" role="2oxUTC" />
+                </node>
+              </node>
+            </node>
+            <node concept="3clFbF" id="5jVx7S1ZK7I" role="3cqZAp">
+              <node concept="2OqwBi" id="5jVx7S1ZLdA" role="3clFbG">
+                <node concept="2OqwBi" id="5jVx7S1ZKkM" role="2Oq$k0">
+                  <node concept="37vLTw" id="5jVx7S1ZK7G" role="2Oq$k0">
+                    <ref role="3cqZAo" node="5jVx7S1Z$Hy" resolve="reit" />
+                  </node>
+                  <node concept="3TrEf2" id="5jVx7S1ZKFR" role="2OqNvi">
+                    <ref role="3Tt5mk" to="jfgh:2aBGSFggvpT" resolve="conclusion" />
+                  </node>
+                </node>
+                <node concept="2oxUTD" id="5jVx7S1ZLGl" role="2OqNvi">
+                  <node concept="2OqwBi" id="5jVx7S1ZTqn" role="2oxUTC">
+                    <node concept="2OqwBi" id="5jVx7S1ZSwB" role="2Oq$k0">
+                      <node concept="2ZBlsa" id="5jVx7S1ZLTz" role="2Oq$k0" />
+                      <node concept="3TrEf2" id="5jVx7S1ZSTW" role="2OqNvi">
+                        <ref role="3Tt5mk" to="jfgh:2aBGSFggvpT" resolve="conclusion" />
+                      </node>
+                    </node>
+                    <node concept="1$rogu" id="5jVx7S1ZTYD" role="2OqNvi" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3clFbF" id="5jVx7S1ZUqm" role="3cqZAp">
+              <node concept="37vLTw" id="5jVx7S1ZUqk" role="3clFbG">
+                <ref role="3cqZAo" node="5jVx7S1Z$Hy" resolve="reit" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="16NfWO" id="5jVx7S1ZUD4" role="upBLP">
+          <node concept="uGdhv" id="5jVx7S1ZUXC" role="16NeZM">
+            <node concept="3clFbS" id="5jVx7S1ZUXE" role="2VODD2">
+              <node concept="3clFbF" id="5jVx7S1ZV64" role="3cqZAp">
+                <node concept="3cpWs3" id="5jVx7S1ZWqG" role="3clFbG">
+                  <node concept="2OqwBi" id="5jVx7S1ZWSf" role="3uHU7w">
+                    <node concept="2ZBlsa" id="5jVx7S1ZWzl" role="2Oq$k0" />
+                    <node concept="3TrcHB" id="5jVx7S1ZXde" role="2OqNvi">
+                      <ref role="3TsBF5" to="jfgh:3JXBM6C54BE" resolve="sequenceNum" />
+                    </node>
+                  </node>
+                  <node concept="Xl_RD" id="5jVx7S1ZV63" role="3uHU7B">
+                    <property role="Xl_RC" value="reiterate " />
+                  </node>
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="16NL0t" id="5jVx7S20Wi_" role="upBLP">
+          <node concept="2h3Zct" id="5jVx7S20X4y" role="16NL0q">
+            <property role="2h4Kg1" value="Reiterate assumption or premise" />
+          </node>
+        </node>
+      </node>
+      <node concept="3Tqbb2" id="5jVx7S1Yvxa" role="2ZBHrp">
+        <ref role="ehGHo" to="jfgh:3JXBM6C3OtS" resolve="Reasoning" />
+      </node>
+      <node concept="2$S_p_" id="5jVx7S1Yv_S" role="2$S_pT">
+        <node concept="3clFbS" id="5jVx7S1Yv_T" role="2VODD2">
+          <node concept="3clFbJ" id="5jVx7S1ZjSa" role="3cqZAp">
+            <node concept="3clFbS" id="5jVx7S1ZjSc" role="3clFbx">
+              <node concept="3cpWs8" id="5jVx7S2079z" role="3cqZAp">
+                <node concept="3cpWsn" id="5jVx7S2079$" role="3cpWs9">
+                  <property role="TrG5h" value="available" />
+                  <node concept="2I9FWS" id="5jVx7S20byr" role="1tU5fm" />
+                  <node concept="2OqwBi" id="5jVx7S208LG" role="33vP2m">
+                    <node concept="2OqwBi" id="5jVx7S2079_" role="2Oq$k0">
+                      <node concept="3zZkjj" id="5jVx7S2079F" role="2OqNvi">
+                        <node concept="1bVj0M" id="5jVx7S2079G" role="23t8la">
+                          <node concept="3clFbS" id="5jVx7S2079H" role="1bW5cS">
+                            <node concept="3clFbF" id="5jVx7S2079I" role="3cqZAp">
+                              <node concept="22lmx$" id="5jVx7S2079J" role="3clFbG">
+                                <node concept="2OqwBi" id="5jVx7S2079K" role="3uHU7w">
+                                  <node concept="37vLTw" id="5jVx7S2079L" role="2Oq$k0">
+                                    <ref role="3cqZAo" node="5jVx7S2079S" resolve="it" />
+                                  </node>
+                                  <node concept="1mIQ4w" id="5jVx7S2079M" role="2OqNvi">
+                                    <node concept="chp4Y" id="5jVx7S2079N" role="cj9EA">
+                                      <ref role="cht4Q" to="jfgh:$u9BK__JRe" resolve="Premise" />
+                                    </node>
+                                  </node>
+                                </node>
+                                <node concept="2OqwBi" id="5jVx7S2079O" role="3uHU7B">
+                                  <node concept="37vLTw" id="5jVx7S2079P" role="2Oq$k0">
+                                    <ref role="3cqZAo" node="5jVx7S2079S" resolve="it" />
+                                  </node>
+                                  <node concept="1mIQ4w" id="5jVx7S2079Q" role="2OqNvi">
+                                    <node concept="chp4Y" id="5jVx7S2079R" role="cj9EA">
+                                      <ref role="cht4Q" to="jfgh:3JXBM6C3Pwi" resolve="Assumption" />
+                                    </node>
+                                  </node>
+                                </node>
+                              </node>
+                            </node>
+                          </node>
+                          <node concept="Rh6nW" id="5jVx7S2079S" role="1bW2Oz">
+                            <property role="TrG5h" value="it" />
+                            <node concept="2jxLKc" id="5jVx7S2079T" role="1tU5fm" />
+                          </node>
+                        </node>
+                      </node>
+                      <node concept="2OqwBi" id="5jVx7S20JJD" role="2Oq$k0">
+                        <node concept="1PxgMI" id="5jVx7S2079C" role="2Oq$k0">
+                          <property role="1BlNFB" value="true" />
+                          <node concept="chp4Y" id="5jVx7S2079D" role="3oSUPX">
+                            <ref role="cht4Q" to="jfgh:3JXBM6C3UQB" resolve="Node" />
+                          </node>
+                          <node concept="3bvxqY" id="5jVx7S2079E" role="1m5AlR" />
+                        </node>
+                        <node concept="2qgKlT" id="5jVx7S20KqM" role="2OqNvi">
+                          <ref role="37wK5l" to="qd7f:5jVx7S20nJ_" resolve="allInScope" />
+                        </node>
+                      </node>
+                    </node>
+                    <node concept="ANE8D" id="5jVx7S209G$" role="2OqNvi" />
+                  </node>
+                </node>
+              </node>
+              <node concept="3cpWs6" id="5jVx7S1Zz6l" role="3cqZAp">
+                <node concept="2OqwBi" id="5jVx7S1Zz6m" role="3cqZAk">
+                  <node concept="37vLTw" id="5jVx7S2079U" role="2Oq$k0">
+                    <ref role="3cqZAo" node="5jVx7S2079$" resolve="available" />
+                  </node>
+                  <node concept="1MD8d$" id="5jVx7S1Zz6G" role="2OqNvi">
+                    <node concept="1bVj0M" id="5jVx7S1Zz6H" role="23t8la">
+                      <node concept="3clFbS" id="5jVx7S1Zz6I" role="1bW5cS">
+                        <node concept="3clFbF" id="5jVx7S1Zz6J" role="3cqZAp">
+                          <node concept="2OqwBi" id="5jVx7S1Zz6K" role="3clFbG">
+                            <node concept="37vLTw" id="5jVx7S1Zz6L" role="2Oq$k0">
+                              <ref role="3cqZAo" node="5jVx7S1Zz6O" resolve="s" />
+                            </node>
+                            <node concept="TSZUe" id="5jVx7S1Zz6M" role="2OqNvi">
+                              <node concept="1PxgMI" id="5jVx7S1ZRjj" role="25WWJ7">
+                                <property role="1BlNFB" value="true" />
+                                <node concept="chp4Y" id="5jVx7S1ZRJX" role="3oSUPX">
+                                  <ref role="cht4Q" to="jfgh:3JXBM6C3OtS" resolve="Reasoning" />
+                                </node>
+                                <node concept="37vLTw" id="5jVx7S1Zz6N" role="1m5AlR">
+                                  <ref role="3cqZAo" node="5jVx7S1Zz6Q" resolve="it" />
+                                </node>
+                              </node>
+                            </node>
+                          </node>
+                        </node>
+                        <node concept="3clFbF" id="5jVx7S20edd" role="3cqZAp">
+                          <node concept="37vLTw" id="5jVx7S20edb" role="3clFbG">
+                            <ref role="3cqZAo" node="5jVx7S1Zz6O" resolve="s" />
+                          </node>
+                        </node>
+                      </node>
+                      <node concept="37vLTG" id="5jVx7S1Zz6O" role="1bW2Oz">
+                        <property role="TrG5h" value="s" />
+                        <node concept="2I9FWS" id="5jVx7S1Zz6P" role="1tU5fm">
+                          <ref role="2I9WkF" to="jfgh:3JXBM6C3OtS" resolve="Reasoning" />
+                        </node>
+                      </node>
+                      <node concept="Rh6nW" id="5jVx7S1Zz6Q" role="1bW2Oz">
+                        <property role="TrG5h" value="it" />
+                        <node concept="2jxLKc" id="5jVx7S1Zz6R" role="1tU5fm" />
+                      </node>
+                    </node>
+                    <node concept="2ShNRf" id="5jVx7S1Zz6S" role="1MDeny">
+                      <node concept="2T8Vx0" id="5jVx7S1Zz6T" role="2ShVmc">
+                        <node concept="2I9FWS" id="5jVx7S1Zz6U" role="2T96Bj">
+                          <ref role="2I9WkF" to="jfgh:3JXBM6C3OtS" resolve="Reasoning" />
+                        </node>
+                      </node>
+                    </node>
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="2OqwBi" id="5jVx7S1Zkfh" role="3clFbw">
+              <node concept="3bvxqY" id="5jVx7S1Zk0c" role="2Oq$k0" />
+              <node concept="1mIQ4w" id="5jVx7S1ZkAb" role="2OqNvi">
+                <node concept="chp4Y" id="5jVx7S1ZkJ7" role="cj9EA">
+                  <ref role="cht4Q" to="jfgh:3JXBM6C3UQB" resolve="Node" />
+                </node>
+              </node>
+            </node>
+          </node>
+          <node concept="3clFbF" id="5jVx7S1ZzvI" role="3cqZAp">
+            <node concept="10Nm6u" id="5jVx7S1ZzvG" role="3clFbG" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="3VyMlK" id="5jVx7S20VFl" role="3ft7WO" />
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps
index 1a950501..2c9fba39 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps
@@ -413,5 +413,13 @@
     <property role="TrG5h" value="Ok" />
     <ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
   </node>
+  <node concept="1TIwiD" id="5jVx7S1Yau5">
+    <property role="EcuMT" value="6123633795074140037" />
+    <property role="3GE5qa" value="proof.reasoning" />
+    <property role="TrG5h" value="Reiteration" />
+    <property role="34LRSv" value="R" />
+    <property role="R4oN_" value="Reiteration" />
+    <ref role="1TJDcQ" node="3JXBM6C3FsA" resolve="Judgement" />
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/types.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/types.mps
index 1a942c70..08487492 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/types.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/types.mps
@@ -981,6 +981,62 @@
         </node>
       </node>
     </node>
+    <node concept="AVZhu" id="5jVx7S22gUI" role="3ArX_J">
+      <property role="TrG5h" value="premise_ok" />
+      <node concept="2t___k" id="5jVx7S22gUJ" role="20_v8_">
+        <ref role="2t_S0q" to="jfgh:$u9BK__JRe" resolve="Premise" />
+        <node concept="3A20r5" id="5jVx7S22gUK" role="2t_VXX">
+          <property role="TrG5h" value="prem" />
+        </node>
+      </node>
+      <node concept="3Aq9E8" id="5jVx7S22gUL" role="3otmyu">
+        <node concept="3I6sU6" id="5jVx7S22gUM" role="3Ip0Jz">
+          <node concept="3I6s7M" id="5jVx7S22gUN" role="3I6sU7">
+            <node concept="1imXTs" id="5jVx7S22gUO" role="3I6s78">
+              <node concept="a7P8L" id="5jVx7S22gUP" role="1imXu6">
+                <ref role="a7OzE" node="5jVx7S22gV3" resolve="Stnc" />
+              </node>
+              <node concept="2OqwBi" id="5jVx7S22gUQ" role="1imXSf">
+                <node concept="3A2sRY" id="5jVx7S22gUR" role="2Oq$k0">
+                  <ref role="3A2yKK" node="5jVx7S22gUK" resolve="prem" />
+                </node>
+                <node concept="3TrEf2" id="5jVx7S22hrC" role="2OqNvi">
+                  <ref role="3Tt5mk" to="jfgh:2aBGSFggvpT" resolve="conclusion" />
+                </node>
+              </node>
+            </node>
+          </node>
+          <node concept="3I6s7M" id="5jVx7S22gUT" role="3I6sU7">
+            <node concept="3Aqt3T" id="5jVx7S22gUU" role="3I6s78">
+              <ref role="3AqCNq" node="2aBGSFgfwNi" resolve="conclusion" />
+              <node concept="a7P8L" id="5jVx7S22gUV" role="3AunhB">
+                <ref role="a7OzE" node="5jVx7S22gV3" resolve="Stnc" />
+              </node>
+              <node concept="3BlFb$" id="5jVx7S22gUW" role="3AunhB">
+                <node concept="3A2sRY" id="5jVx7S22gUX" role="3BlFb_">
+                  <ref role="3A2yKK" node="5jVx7S22gUK" resolve="prem" />
+                </node>
+              </node>
+            </node>
+          </node>
+          <node concept="3I6s7M" id="5jVx7S22gUY" role="3I6sU7">
+            <node concept="3Aqt3T" id="5jVx7S22gUZ" role="3I6s78">
+              <ref role="3AqCNq" node="2YqrT$P7tud" resolve="valid" />
+              <node concept="3BlFb$" id="5jVx7S22gV0" role="3AunhB">
+                <node concept="3A2sRY" id="5jVx7S22gV1" role="3BlFb_">
+                  <ref role="3A2yKK" node="5jVx7S22gUK" resolve="prem" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="3NuqgR" id="5jVx7S22gV2" role="3Nuqhd">
+          <node concept="aZer4" id="5jVx7S22gV3" role="3XD1gS">
+            <property role="TrG5h" value="Stnc" />
+          </node>
+        </node>
+      </node>
+    </node>
     <node concept="AVZhu" id="2aBGSFgfACW" role="3ArX_J">
       <property role="TrG5h" value="Judgement_conclusion" />
       <node concept="3Aq9E8" id="2aBGSFgfAEo" role="3otmyu">
@@ -1027,6 +1083,136 @@
         </node>
       </node>
     </node>
+    <node concept="AVZhu" id="5jVx7S216YY" role="3ArX_J">
+      <property role="TrG5h" value="reiteration_valid" />
+      <node concept="3Aq9E8" id="5jVx7S21uiY" role="3otmyu">
+        <node concept="3I6sU6" id="5jVx7S21uiZ" role="3Ip0Jz">
+          <node concept="3I6s7M" id="5jVx7S21uj3" role="3I6sU7">
+            <node concept="3Aqt3T" id="5jVx7S21uj2" role="3I6s78">
+              <ref role="3AqCNq" node="2YqrT$P7tud" resolve="valid" />
+              <node concept="3BlFb$" id="5jVx7S21uj8" role="3AunhB">
+                <node concept="3A2sRY" id="5jVx7S21ujh" role="3BlFb_">
+                  <ref role="3A2yKK" node="5jVx7S2178P" resolve="reit" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="3Aq93q" id="5jVx7S217sJ" role="3orSU4">
+        <property role="3ArMco" value="true" />
+        <node concept="3I6sU6" id="5jVx7S217sK" role="3Ip0Jz">
+          <node concept="3I6s7M" id="5jVx7S21O1J" role="3I6sU7">
+            <node concept="3Aqt3T" id="5jVx7S21O1H" role="3I6s78">
+              <ref role="3AqCNq" node="2aBGSFgfwNi" resolve="conclusion" />
+              <node concept="a7P8L" id="5jVx7S21O24" role="3AunhB">
+                <ref role="a7OzE" node="5jVx7S21pW_" resolve="Con" />
+              </node>
+              <node concept="3BlFb$" id="5jVx7S21O2a" role="3AunhB">
+                <node concept="3A2sRY" id="5jVx7S21O2k" role="3BlFb_">
+                  <ref role="3A2yKK" node="5jVx7S2178P" resolve="reit" />
+                </node>
+              </node>
+            </node>
+          </node>
+          <node concept="3I6s7M" id="5jVx7S217t5" role="3I6sU7">
+            <node concept="3Aqt3T" id="5jVx7S217t4" role="3I6s78">
+              <ref role="3AqCNq" node="2aBGSFgfwNi" resolve="conclusion" />
+              <node concept="1uarlV" id="5jVx7S21pWO" role="3AunhB">
+                <node concept="a7P8L" id="5jVx7S21je4" role="1uarlU">
+                  <ref role="a7OzE" node="5jVx7S217sP" resolve="Ass" />
+                </node>
+                <node concept="a7P8L" id="5jVx7S21pX8" role="1uarlW">
+                  <ref role="a7OzE" node="5jVx7S21pW_" resolve="Con" />
+                </node>
+              </node>
+              <node concept="3BlFb$" id="5jVx7S21jec" role="3AunhB">
+                <node concept="2OqwBi" id="5jVx7S21pr9" role="3BlFb_">
+                  <node concept="2OqwBi" id="5jVx7S21lHO" role="2Oq$k0">
+                    <node concept="2OqwBi" id="5jVx7S21jnV" role="2Oq$k0">
+                      <node concept="3A2sRY" id="5jVx7S21jem" role="2Oq$k0">
+                        <ref role="3A2yKK" node="5jVx7S2178P" resolve="reit" />
+                      </node>
+                      <node concept="3Tsc0h" id="5jVx7S21kbH" role="2OqNvi">
+                        <ref role="3TtcxE" to="jfgh:3JXBM6C3MQ0" resolve="premise" />
+                      </node>
+                    </node>
+                    <node concept="1uHKPH" id="5jVx7S21nFd" role="2OqNvi" />
+                  </node>
+                  <node concept="3TrEf2" id="5jVx7S21pUp" role="2OqNvi">
+                    <ref role="3Tt5mk" to="jfgh:3JXBM6C3FuH" resolve="reasoning" />
+                  </node>
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="3NuqgR" id="5jVx7S217sO" role="3Nuqhd">
+          <node concept="aZer4" id="5jVx7S21pW_" role="3XD1gS">
+            <property role="TrG5h" value="Con" />
+          </node>
+          <node concept="aZer4" id="5jVx7S217sP" role="3XD1gS">
+            <property role="TrG5h" value="Ass" />
+          </node>
+        </node>
+      </node>
+      <node concept="3Aq93q" id="5jVx7S21pWi" role="3orSU4">
+        <property role="3ArMco" value="true" />
+        <node concept="3I6sU6" id="5jVx7S21pWj" role="3Ip0Jz">
+          <node concept="3I6s7M" id="5jVx7S21pXe" role="3I6sU7">
+            <node concept="3Aqt3T" id="5jVx7S21pXd" role="3I6s78">
+              <ref role="3AqCNq" node="2YqrT$P7tud" resolve="valid" />
+              <node concept="3BlFb$" id="5jVx7S21pXj" role="3AunhB">
+                <node concept="2OqwBi" id="5jVx7S21SqX" role="3BlFb_">
+                  <node concept="2OqwBi" id="5jVx7S21si9" role="2Oq$k0">
+                    <node concept="2OqwBi" id="5jVx7S21q71" role="2Oq$k0">
+                      <node concept="3A2sRY" id="5jVx7S21pXs" role="2Oq$k0">
+                        <ref role="3A2yKK" node="5jVx7S2178P" resolve="reit" />
+                      </node>
+                      <node concept="3Tsc0h" id="5jVx7S21qHJ" role="2OqNvi">
+                        <ref role="3TtcxE" to="jfgh:3JXBM6C3MQ0" resolve="premise" />
+                      </node>
+                    </node>
+                    <node concept="1uHKPH" id="5jVx7S21uib" role="2OqNvi" />
+                  </node>
+                  <node concept="3TrEf2" id="5jVx7S21T6N" role="2OqNvi">
+                    <ref role="3Tt5mk" to="jfgh:3JXBM6C3FuH" resolve="reasoning" />
+                  </node>
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2t___k" id="5jVx7S2178O" role="20_v8_">
+        <ref role="2t_S0q" to="jfgh:5jVx7S1Yau5" resolve="Reiteration" />
+        <node concept="3A20r5" id="5jVx7S2178P" role="2t_VXX">
+          <property role="TrG5h" value="reit" />
+        </node>
+      </node>
+      <node concept="cBwPQ" id="5jVx7S217t8" role="30RCb4">
+        <node concept="3clFbS" id="5jVx7S217t9" role="16YjZG">
+          <node concept="3clFbF" id="5jVx7S217tm" role="3cqZAp">
+            <node concept="3clFbC" id="5jVx7S21iTF" role="3clFbG">
+              <node concept="3cmrfG" id="5jVx7S21iTU" role="3uHU7w">
+                <property role="3cmrfH" value="1" />
+              </node>
+              <node concept="2OqwBi" id="5jVx7S219L5" role="3uHU7B">
+                <node concept="2OqwBi" id="5jVx7S217D2" role="2Oq$k0">
+                  <node concept="3A2sRY" id="5jVx7S217tl" role="2Oq$k0">
+                    <ref role="3A2yKK" node="5jVx7S2178P" resolve="reit" />
+                  </node>
+                  <node concept="3Tsc0h" id="5jVx7S217Wz" role="2OqNvi">
+                    <ref role="3TtcxE" to="jfgh:3JXBM6C3MQ0" resolve="premise" />
+                  </node>
+                </node>
+                <node concept="34oBXx" id="5jVx7S21d8X" role="2OqNvi" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
     <node concept="AVZhu" id="2aBGSFgfrJr" role="3ArX_J">
       <property role="TrG5h" value="orIntro_valid1" />
       <node concept="3Aq93q" id="2aBGSFgfwOr" role="3orSU4">
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.sandbox.mps b/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.sandbox.mps
index e75aa312..1c2101bb 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.sandbox.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.sandbox.mps
@@ -42,6 +42,7 @@
       <concept id="657004910291159432" name="jetbrains.mps.fitch.structure.Goal" flags="ng" index="GyqZO">
         <child id="657004910291159433" name="sentence" index="GyqZP" />
       </concept>
+      <concept id="6123633795074140037" name="jetbrains.mps.fitch.structure.Reiteration" flags="ng" index="1l0MfV" />
     </language>
     <language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
       <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
@@ -58,7 +59,7 @@
             <node concept="2jWLFD" id="3JXBM6C4ztH" role="2jWM__">
               <property role="TrG5h" value="p" />
             </node>
-            <node concept="2jWLFQ" id="3JXBM6C4ztI" role="2jWM__">
+            <node concept="2jWLFQ" id="5jVx7S2251s" role="2jWM__">
               <node concept="2jWLFD" id="3JXBM6C4ztJ" role="2jWLFT">
                 <property role="TrG5h" value="p" />
               </node>
@@ -117,14 +118,17 @@
             <property role="TrG5h" value="p" />
           </node>
         </node>
-        <node concept="2jWGsN" id="$u9BK_y$eJ" role="2jWza4">
-          <node concept="2jWLFQ" id="$u9BK_y$eK" role="3MT$nN">
-            <node concept="2jWM$7" id="$u9BK_y$eL" role="2jWLFT">
-              <node concept="2jWLFD" id="$u9BK_y$eM" role="2jWM__">
+        <node concept="1l0MfV" id="5jVx7S2165V" role="2jWza4">
+          <node concept="2jWMwi" id="5jVx7S2165W" role="2jWFax">
+            <ref role="2jWMyc" node="3JXBM6C4ztF" />
+          </node>
+          <node concept="2jWLFQ" id="5jVx7S2165X" role="3MT$nN">
+            <node concept="2jWM$7" id="5jVx7S2165Y" role="2jWLFT">
+              <node concept="2jWLFD" id="5jVx7S2165Z" role="2jWM__">
                 <property role="TrG5h" value="p" />
               </node>
-              <node concept="2jWLFQ" id="$u9BK_y$eN" role="2jWM__">
-                <node concept="2jWLFD" id="$u9BK_y$eO" role="2jWLFT">
+              <node concept="2jWLFQ" id="5jVx7S21660" role="2jWM__">
+                <node concept="2jWLFD" id="5jVx7S21661" role="2jWLFT">
                   <property role="TrG5h" value="p" />
                 </node>
               </node>
@@ -136,8 +140,8 @@
         <node concept="2jWMwi" id="$u9BK_yzWV" role="2jWFax">
           <ref role="2jWMyc" node="3JXBM6Ca7rQ" />
         </node>
-        <node concept="2jWMwi" id="$u9BK_y$kI" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$eJ" />
+        <node concept="2jWMwi" id="5jVx7S2166q" role="2jWFax">
+          <ref role="2jWMyc" node="5jVx7S2165V" />
         </node>
         <node concept="2jWM_K" id="$u9BK_yzWw" role="3MT$nN">
           <node concept="2jWLFD" id="$u9BK_yzWs" role="2jWM_N">
@@ -270,14 +274,17 @@
             </node>
           </node>
         </node>
-        <node concept="2jWGsN" id="$u9BK_y$z8" role="2jWza4">
-          <node concept="2jWLFQ" id="$u9BK_y$z9" role="3MT$nN">
-            <node concept="2jWM$7" id="$u9BK_y$za" role="2jWLFT">
-              <node concept="2jWLFD" id="$u9BK_y$zb" role="2jWM__">
+        <node concept="1l0MfV" id="5jVx7S22tDg" role="2jWza4">
+          <node concept="2jWMwi" id="5jVx7S22tDh" role="2jWFax">
+            <ref role="2jWMyc" node="$u9BK_y$yH" />
+          </node>
+          <node concept="2jWLFQ" id="5jVx7S22tDi" role="3MT$nN">
+            <node concept="2jWM$7" id="5jVx7S22tDj" role="2jWLFT">
+              <node concept="2jWLFD" id="5jVx7S22tDk" role="2jWM__">
                 <property role="TrG5h" value="p" />
               </node>
-              <node concept="2jWLFQ" id="$u9BK_y$zc" role="2jWM__">
-                <node concept="2jWLFD" id="$u9BK_y$zd" role="2jWLFT">
+              <node concept="2jWLFQ" id="5jVx7S22tDl" role="2jWM__">
+                <node concept="2jWLFD" id="5jVx7S22tDm" role="2jWLFT">
                   <property role="TrG5h" value="p" />
                 </node>
               </node>
@@ -289,8 +296,8 @@
         <node concept="2jWMwi" id="$u9BK_y$zf" role="2jWFax">
           <ref role="2jWMyc" node="$u9BK_y$z6" />
         </node>
-        <node concept="2jWMwi" id="$u9BK_y$zg" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$z8" />
+        <node concept="2jWMwi" id="5jVx7S22tDL" role="2jWFax">
+          <ref role="2jWMyc" node="5jVx7S22tDg" />
         </node>
         <node concept="2jWM_K" id="$u9BK_y$zh" role="3MT$nN">
           <node concept="2jWLFQ" id="$u9BK_y$__" role="2jWM_N">