diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps
index be4498a6..db6bde03 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/behavior.mps
@@ -33,17 +33,20 @@
       <concept id="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
         <child id="1137022507850" name="body" index="2VODD2" />
       </concept>
+      <concept id="1070534644030" name="jetbrains.mps.baseLanguage.structure.BooleanType" flags="in" index="10P_77" />
       <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>
       <concept id="1068580123132" name="jetbrains.mps.baseLanguage.structure.BaseMethodDeclaration" flags="ng" index="3clF44">
         <child id="1068580123133" name="returnType" index="3clF45" />
+        <child id="1068580123134" name="parameter" index="3clF46" />
         <child id="1068580123135" name="body" index="3clF47" />
       </concept>
       <concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
@@ -82,6 +85,7 @@
         <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="6677504323281689838" name="jetbrains.mps.lang.smodel.structure.SConceptType" flags="in" index="3bZ5Sz" />
       <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" />
@@ -189,5 +193,24 @@
       <node concept="3clFbS" id="5jVx7S20nJs" role="2VODD2" />
     </node>
   </node>
+  <node concept="13h7C7" id="3w0n0hzjKLx">
+    <property role="3GE5qa" value="proof" />
+    <ref role="13h7C2" to="jfgh:3JXBM6C5urr" resolve="Root" />
+    <node concept="13i0hz" id="3w0n0hzjKLG" role="13h7CS">
+      <property role="13i0iv" value="true" />
+      <property role="13i0it" value="true" />
+      <property role="TrG5h" value="isRuleSupported" />
+      <node concept="37vLTG" id="3w0n0hzjKN7" role="3clF46">
+        <property role="TrG5h" value="ruleConcept" />
+        <node concept="3bZ5Sz" id="3w0n0hzjKO0" role="1tU5fm" />
+      </node>
+      <node concept="3Tm1VV" id="3w0n0hzjKLH" role="1B3o_S" />
+      <node concept="10P_77" id="3w0n0hzjKLW" role="3clF45" />
+      <node concept="3clFbS" id="3w0n0hzjKLJ" role="3clF47" />
+    </node>
+    <node concept="13hLZK" id="3w0n0hzjKLy" role="13h7CW">
+      <node concept="3clFbS" id="3w0n0hzjKLz" 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 95423253..a19eed9d 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/constraints.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/constraints.mps
@@ -344,59 +344,6 @@
       </node>
     </node>
   </node>
-  <node concept="1M2fIO" id="3JXBM6C4VbD">
-    <property role="3GE5qa" value="proof" />
-    <ref role="1M2myG" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
-    <node concept="EnEH3" id="3JXBM6C4VbE" role="1MhHOB">
-      <ref role="EomxK" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
-      <node concept="Eqf_E" id="3JXBM6C4VbG" role="EtsB7">
-        <node concept="3clFbS" id="3JXBM6C4VbH" role="2VODD2">
-          <node concept="3clFbF" id="3JXBM6C4VsJ" role="3cqZAp">
-            <node concept="2OqwBi" id="3JXBM6C4VsQ" role="3clFbG">
-              <node concept="2OqwBi" id="3JXBM6C4VsR" role="2Oq$k0">
-                <node concept="EsrRn" id="3JXBM6C4VsS" role="2Oq$k0" />
-                <node concept="3Tsc0h" id="3JXBM6C4VsT" role="2OqNvi">
-                  <ref role="3TtcxE" to="jfgh:3JXBM6C4wQA" resolve="content" />
-                </node>
-              </node>
-              <node concept="1MD8d$" id="3JXBM6C4VsU" role="2OqNvi">
-                <node concept="1bVj0M" id="3JXBM6C4VsV" role="23t8la">
-                  <node concept="3clFbS" id="3JXBM6C4VsW" role="1bW5cS">
-                    <node concept="3clFbF" id="3JXBM6C4VsX" role="3cqZAp">
-                      <node concept="3cpWs3" id="3JXBM6C4VsY" role="3clFbG">
-                        <node concept="2OqwBi" id="3JXBM6C4VsZ" role="3uHU7w">
-                          <node concept="37vLTw" id="3JXBM6C4Vt0" role="2Oq$k0">
-                            <ref role="3cqZAo" node="3JXBM6C4Vt5" resolve="it" />
-                          </node>
-                          <node concept="3TrcHB" id="3JXBM6C4Vt1" role="2OqNvi">
-                            <ref role="3TsBF5" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
-                          </node>
-                        </node>
-                        <node concept="37vLTw" id="3JXBM6C4Vt2" role="3uHU7B">
-                          <ref role="3cqZAo" node="3JXBM6C4Vt3" resolve="s" />
-                        </node>
-                      </node>
-                    </node>
-                  </node>
-                  <node concept="37vLTG" id="3JXBM6C4Vt3" role="1bW2Oz">
-                    <property role="TrG5h" value="s" />
-                    <node concept="10Oyi0" id="3JXBM6C4Vt4" role="1tU5fm" />
-                  </node>
-                  <node concept="Rh6nW" id="3JXBM6C4Vt5" role="1bW2Oz">
-                    <property role="TrG5h" value="it" />
-                    <node concept="2jxLKc" id="3JXBM6C4Vt6" role="1tU5fm" />
-                  </node>
-                </node>
-                <node concept="3cmrfG" id="3JXBM6C4Vt7" role="1MDeny">
-                  <property role="3cmrfH" value="0" />
-                </node>
-              </node>
-            </node>
-          </node>
-        </node>
-      </node>
-    </node>
-  </node>
   <node concept="1M2fIO" id="5jVx7S22QGW">
     <property role="3GE5qa" value="proof.reasoning" />
     <ref role="1M2myG" to="jfgh:3JXBM6C3Pwi" resolve="Assumption" />
@@ -501,5 +448,58 @@
       </node>
     </node>
   </node>
+  <node concept="1M2fIO" id="3w0n0hzhUPi">
+    <property role="3GE5qa" value="proof" />
+    <ref role="1M2myG" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
+    <node concept="EnEH3" id="3JXBM6C4VbE" role="1MhHOB">
+      <ref role="EomxK" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
+      <node concept="Eqf_E" id="3JXBM6C4VbG" role="EtsB7">
+        <node concept="3clFbS" id="3JXBM6C4VbH" role="2VODD2">
+          <node concept="3clFbF" id="3JXBM6C4VsJ" role="3cqZAp">
+            <node concept="2OqwBi" id="3JXBM6C4VsQ" role="3clFbG">
+              <node concept="2OqwBi" id="3JXBM6C4VsR" role="2Oq$k0">
+                <node concept="EsrRn" id="3JXBM6C4VsS" role="2Oq$k0" />
+                <node concept="3Tsc0h" id="3JXBM6C4VsT" role="2OqNvi">
+                  <ref role="3TtcxE" to="jfgh:3JXBM6C4wQA" resolve="content" />
+                </node>
+              </node>
+              <node concept="1MD8d$" id="3JXBM6C4VsU" role="2OqNvi">
+                <node concept="1bVj0M" id="3JXBM6C4VsV" role="23t8la">
+                  <node concept="3clFbS" id="3JXBM6C4VsW" role="1bW5cS">
+                    <node concept="3clFbF" id="3JXBM6C4VsX" role="3cqZAp">
+                      <node concept="3cpWs3" id="3JXBM6C4VsY" role="3clFbG">
+                        <node concept="2OqwBi" id="3JXBM6C4VsZ" role="3uHU7w">
+                          <node concept="37vLTw" id="3JXBM6C4Vt0" role="2Oq$k0">
+                            <ref role="3cqZAo" node="3JXBM6C4Vt5" resolve="it" />
+                          </node>
+                          <node concept="3TrcHB" id="3JXBM6C4Vt1" role="2OqNvi">
+                            <ref role="3TsBF5" to="jfgh:3JXBM6C4nuA" resolve="contentSize" />
+                          </node>
+                        </node>
+                        <node concept="37vLTw" id="3JXBM6C4Vt2" role="3uHU7B">
+                          <ref role="3cqZAo" node="3JXBM6C4Vt3" resolve="s" />
+                        </node>
+                      </node>
+                    </node>
+                  </node>
+                  <node concept="37vLTG" id="3JXBM6C4Vt3" role="1bW2Oz">
+                    <property role="TrG5h" value="s" />
+                    <node concept="10Oyi0" id="3JXBM6C4Vt4" role="1tU5fm" />
+                  </node>
+                  <node concept="Rh6nW" id="3JXBM6C4Vt5" role="1bW2Oz">
+                    <property role="TrG5h" value="it" />
+                    <node concept="2jxLKc" id="3JXBM6C4Vt6" role="1tU5fm" />
+                  </node>
+                </node>
+                <node concept="3cmrfG" id="3JXBM6C4Vt7" role="1MDeny">
+                  <property role="3cmrfH" value="0" />
+                </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 867d7ad9..53a00ea2 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/editor.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/editor.mps
@@ -10,7 +10,6 @@
   <imports>
     <import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
     <import index="wyt6" ref="6354ebe7-c22a-4a0f-ac54-50b52ab9b065/java:java.lang(JDK/)" implicit="true" />
-    <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" 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>
@@ -34,8 +33,6 @@
       <concept id="1196434649611" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_SimpleString" flags="ng" index="2h3Zct">
         <property id="1196434851095" name="text" index="2h4Kg1" />
       </concept>
-      <concept id="1106270549637" name="jetbrains.mps.lang.editor.structure.CellLayout_Horizontal" flags="nn" index="2iRfu4" />
-      <concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
       <concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
       <concept id="1237307900041" name="jetbrains.mps.lang.editor.structure.IndentLayoutIndentStyleClassItem" flags="ln" index="lj46D" />
       <concept id="1237308012275" name="jetbrains.mps.lang.editor.structure.IndentLayoutNewLineStyleClassItem" flags="ln" index="ljvvj" />
@@ -99,7 +96,6 @@
       <concept id="1219226236603" name="jetbrains.mps.lang.editor.structure.DrawBracketsStyleClassItem" flags="ln" index="3vyZuw" />
       <concept id="5425882385312046132" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_SubstituteMenu_CurrentTargetNode" flags="nn" index="1yR$tW" />
       <concept id="1139848536355" name="jetbrains.mps.lang.editor.structure.CellModel_WithRole" flags="ng" index="1$h60E">
-        <property id="1139852716018" name="noTargetText" index="1$x2rV" />
         <reference id="1140103550593" name="relationDeclaration" index="1NtTu8" />
       </concept>
       <concept id="7667708318090725848" name="jetbrains.mps.lang.editor.structure.IndentLayoutIndentAnchorStyleClassItem" flags="ln" index="1Bsynf" />
@@ -114,7 +110,6 @@
         <property id="1082639509531" name="nullText" index="ilYzB" />
         <property id="1073389577007" name="text" index="3F0ifm" />
       </concept>
-      <concept id="1073389658414" name="jetbrains.mps.lang.editor.structure.CellModel_Property" flags="sg" stub="730538219796134133" index="3F0A7n" />
       <concept id="1219418625346" name="jetbrains.mps.lang.editor.structure.IStyleContainer" flags="ng" index="3F0Thp">
         <child id="1219418656006" name="styleItem" index="3F10Kt" />
       </concept>
@@ -380,148 +375,6 @@
       </node>
     </node>
   </node>
-  <node concept="24kQdi" id="3JXBM6C3URg">
-    <property role="3GE5qa" value="proof" />
-    <ref role="1XX52x" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
-    <node concept="3EZMnI" id="3JXBM6C3URi" role="2wV5jI">
-      <node concept="3F0A7n" id="3JXBM6C4h$I" role="3EZMnx">
-        <ref role="1NtTu8" to="tpck:h0TrG11" resolve="name" />
-        <node concept="ljvvj" id="3JXBM6C4h$R" role="3F10Kt">
-          <property role="VOm3f" value="true" />
-        </node>
-      </node>
-      <node concept="3F0ifn" id="2AfSc6Jvjpp" role="3EZMnx">
-        <property role="3F0ifm" value="" />
-        <node concept="ljvvj" id="2AfSc6Jvjpq" role="3F10Kt">
-          <property role="VOm3f" value="true" />
-        </node>
-      </node>
-      <node concept="3F0A7n" id="2AfSc6Jvjoy" role="3EZMnx">
-        <ref role="1NtTu8" to="jfgh:2AfSc6Jvjow" resolve="description" />
-        <node concept="ljvvj" id="2AfSc6Jvjs0" role="3F10Kt">
-          <property role="VOm3f" value="true" />
-        </node>
-      </node>
-      <node concept="3F0ifn" id="$u9BK__SIy" role="3EZMnx">
-        <property role="3F0ifm" value="" />
-        <node concept="ljvvj" id="$u9BK__SJr" role="3F10Kt">
-          <property role="VOm3f" value="true" />
-        </node>
-      </node>
-      <node concept="3EZMnI" id="$u9BK__SDZ" role="3EZMnx">
-        <node concept="ljvvj" id="$u9BK__SHA" role="3F10Kt">
-          <property role="VOm3f" value="true" />
-        </node>
-        <node concept="VPM3Z" id="$u9BK__SE1" role="3F10Kt">
-          <property role="VOm3f" value="false" />
-        </node>
-        <node concept="3F0ifn" id="$u9BK__SFC" role="3EZMnx">
-          <property role="3F0ifm" value="Goal:" />
-        </node>
-        <node concept="l2Vlx" id="$u9BK__SE4" role="2iSdaV" />
-        <node concept="3F1sOY" id="$u9BK__SCz" role="3EZMnx">
-          <property role="1$x2rV" value="&lt;no goal&gt;" />
-          <ref role="1NtTu8" to="jfgh:$u9BK__SAr" resolve="goal" />
-        </node>
-      </node>
-      <node concept="3EZMnI" id="$u9BK__SGu" role="3EZMnx">
-        <node concept="VPM3Z" id="$u9BK__SGw" role="3F10Kt">
-          <property role="VOm3f" value="false" />
-        </node>
-        <node concept="ljvvj" id="$u9BK__SHv" role="3F10Kt">
-          <property role="VOm3f" value="true" />
-        </node>
-        <node concept="3F0ifn" id="$u9BK__SHp" role="3EZMnx">
-          <property role="3F0ifm" value="Proof:" />
-        </node>
-        <node concept="l2Vlx" id="$u9BK__SGz" role="2iSdaV" />
-      </node>
-      <node concept="3EZMnI" id="$u9BK_yCN6" role="3EZMnx">
-        <node concept="3EZMnI" id="$u9BK_z1QP" role="3EZMnx">
-          <node concept="VPM3Z" id="$u9BK_z1QR" role="3F10Kt">
-            <property role="VOm3f" value="false" />
-          </node>
-          <node concept="2iRkQZ" id="$u9BK_z1QU" role="2iSdaV" />
-          <node concept="3EZMnI" id="$u9BK_z6et" role="3EZMnx">
-            <node concept="l2Vlx" id="$u9BK_z6eu" role="2iSdaV" />
-            <node concept="VPM3Z" id="$u9BK_z6ev" role="3F10Kt">
-              <property role="VOm3f" value="false" />
-            </node>
-            <node concept="3F2HdR" id="$u9BK_z6ez" role="3EZMnx">
-              <property role="2czwfO" value=" " />
-              <ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
-              <node concept="l2Vlx" id="$u9BK_z6e$" role="2czzBx" />
-              <node concept="tppnM" id="$u9BK_zt0T" role="sWeuL">
-                <node concept="ljvvj" id="$u9BK_zt0V" role="3F10Kt">
-                  <property role="VOm3f" value="true" />
-                </node>
-              </node>
-              <node concept="2w$q5c" id="5RfK0kxj3Yz" role="78xua">
-                <node concept="2aJ2om" id="5RfK0kxj3Y$" role="2w$qW5">
-                  <ref role="2$4xQ3" node="$u9BK_z27v" resolve="ID" />
-                </node>
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="3EZMnI" id="$u9BK_yCN7" role="3EZMnx">
-          <node concept="VPM3Z" id="$u9BK_yCN8" role="3F10Kt">
-            <property role="VOm3f" value="false" />
-          </node>
-          <node concept="2iRkQZ" id="$u9BK_yCNa" role="2iSdaV" />
-          <node concept="3EZMnI" id="3JXBM6C6j0E" role="3EZMnx">
-            <node concept="VPM3Z" id="3JXBM6C6j0G" role="3F10Kt">
-              <property role="VOm3f" value="false" />
-            </node>
-            <node concept="l2Vlx" id="3JXBM6C6j0J" role="2iSdaV" />
-            <node concept="3F2HdR" id="3JXBM6C3URp" role="3EZMnx">
-              <property role="2czwfO" value=" " />
-              <ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
-              <node concept="l2Vlx" id="3JXBM6C3URr" role="2czzBx" />
-              <node concept="tppnM" id="3JXBM6C3URw" role="sWeuL">
-                <node concept="ljvvj" id="3JXBM6C3URy" role="3F10Kt">
-                  <property role="VOm3f" value="true" />
-                </node>
-              </node>
-              <node concept="3F0ifn" id="3JXBM6C3UR$" role="2czzBI">
-                <property role="3F0ifm" value="" />
-                <property role="ilYzB" value="&lt;no steps&gt;" />
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="2iRfu4" id="$u9BK_yCNb" role="2iSdaV" />
-        <node concept="3EZMnI" id="$u9BK_zG5o" role="3EZMnx">
-          <node concept="3EZMnI" id="$u9BK_$Qxk" role="3EZMnx">
-            <node concept="l2Vlx" id="$u9BK_$Qxl" role="2iSdaV" />
-            <node concept="VPM3Z" id="$u9BK_$Qxm" role="3F10Kt">
-              <property role="VOm3f" value="false" />
-            </node>
-            <node concept="3F2HdR" id="$u9BK_$Qxn" role="3EZMnx">
-              <property role="2czwfO" value=" " />
-              <ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
-              <node concept="l2Vlx" id="$u9BK_$Qxo" role="2czzBx" />
-              <node concept="tppnM" id="$u9BK_$Qxp" role="sWeuL">
-                <node concept="ljvvj" id="$u9BK_$Qxq" role="3F10Kt">
-                  <property role="VOm3f" value="true" />
-                </node>
-              </node>
-              <node concept="2w$q5c" id="$u9BK_$QxA" role="78xua">
-                <node concept="2aJ2om" id="$u9BK_$QxB" role="2w$qW5">
-                  <ref role="2$4xQ3" node="$u9BK_zG6f" resolve="BASIS" />
-                </node>
-              </node>
-            </node>
-          </node>
-          <node concept="VPM3Z" id="$u9BK_zG5q" role="3F10Kt">
-            <property role="VOm3f" value="false" />
-          </node>
-          <node concept="2iRkQZ" id="$u9BK_zG5t" role="2iSdaV" />
-        </node>
-      </node>
-      <node concept="l2Vlx" id="3JXBM6C3URl" role="2iSdaV" />
-    </node>
-  </node>
   <node concept="3p36aQ" id="3JXBM6C6A54">
     <property role="3GE5qa" value="proof.reasoning" />
     <ref role="aqKnT" to="jfgh:3JXBM6C3FsN" resolve="Reference" />
@@ -575,10 +428,6 @@
       </node>
     </node>
   </node>
-  <node concept="3p36aQ" id="3JXBM6C6F7z">
-    <property role="3GE5qa" value="proof" />
-    <ref role="aqKnT" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
-  </node>
   <node concept="3p36aQ" id="3JXBM6C6Hgb">
     <property role="3GE5qa" value="proof" />
     <ref role="aqKnT" to="jfgh:3JXBM6C3UQ$" resolve="SubProof" />
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps b/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps
index 27165e36..30d5868c 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/models/structure.mps
@@ -6,7 +6,7 @@
     <devkit ref="78434eb8-b0e5-444b-850d-e7c4ad2da9ab(jetbrains.mps.devkit.aspect.structure)" />
   </languages>
   <imports>
-    <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
+    <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
   </imports>
   <registry>
     <language id="c72da2b9-7cce-4447-8389-f407dc1158b7" name="jetbrains.mps.lang.structure">
@@ -26,7 +26,6 @@
         <reference id="1169127628841" name="intfc" index="PrY4T" />
       </concept>
       <concept id="1071489090640" name="jetbrains.mps.lang.structure.structure.ConceptDeclaration" flags="ig" index="1TIwiD">
-        <property id="1096454100552" name="rootable" index="19KtqR" />
         <reference id="1071489389519" name="extends" index="1TJDcQ" />
         <child id="1169129564478" name="implements" index="PzmwI" />
       </concept>
@@ -51,38 +50,6 @@
       </concept>
     </language>
   </registry>
-  <node concept="1TIwiD" id="3JXBM6C3Fs$">
-    <property role="EcuMT" value="4322786184247818020" />
-    <property role="TrG5h" value="Proof" />
-    <property role="19KtqR" value="true" />
-    <property role="34LRSv" value="proof" />
-    <property role="3GE5qa" value="proof" />
-    <ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
-    <node concept="1TJgyi" id="2AfSc6Jvjow" role="1TKVEl">
-      <property role="IQ2nx" value="2994859399702197792" />
-      <property role="TrG5h" value="description" />
-      <ref role="AX2Wp" to="tpck:fKAOsGN" resolve="string" />
-    </node>
-    <node concept="1TJgyj" id="$u9BK__SAr" role="1TKVEi">
-      <property role="IQ2ns" value="657004910291159451" />
-      <property role="20lmBu" value="aggregation" />
-      <property role="20kJfa" value="goal" />
-      <ref role="20lvS9" node="$u9BK__SA8" resolve="Goal" />
-    </node>
-    <node concept="1TJgyj" id="3JXBM6C4wQA" role="1TKVEi">
-      <property role="IQ2ns" value="4322786184248036774" />
-      <property role="20lmBu" value="aggregation" />
-      <property role="20kJfa" value="content" />
-      <property role="20lbJX" value="1..n" />
-      <ref role="20lvS9" node="3JXBM6C3UQB" resolve="Node" />
-    </node>
-    <node concept="PrWs8" id="3JXBM6C3URC" role="PzmwI">
-      <ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
-    </node>
-    <node concept="PrWs8" id="3JXBM6C5v8v" role="PzmwI">
-      <ref role="PrY4T" node="3JXBM6C5urr" resolve="Root" />
-    </node>
-  </node>
   <node concept="1TIwiD" id="3JXBM6C3FsA">
     <property role="EcuMT" value="4322786184247818022" />
     <property role="TrG5h" value="Judgement" />
@@ -182,7 +149,7 @@
   </node>
   <node concept="PlHQZ" id="3JXBM6C5urr">
     <property role="EcuMT" value="4322786184248288987" />
-    <property role="3GE5qa" value="proof.rule" />
+    <property role="3GE5qa" value="proof" />
     <property role="TrG5h" value="Root" />
     <node concept="PrWs8" id="3JXBM6C5urs" role="PrDN$">
       <ref role="PrY4T" node="3JXBM6C3UQB" resolve="Node" />
@@ -229,5 +196,37 @@
     <property role="EcuMT" value="5505606474791964545" />
     <property role="TrG5h" value="Sentence" />
   </node>
+  <node concept="1TIwiD" id="3w0n0hzgWvH">
+    <property role="EcuMT" value="4035326440038975469" />
+    <property role="3GE5qa" value="proof" />
+    <property role="TrG5h" value="AbstractProof" />
+    <property role="R5$K7" value="true" />
+    <property role="R5$K2" value="false" />
+    <ref role="1TJDcQ" to="tpck:gw2VY9q" resolve="BaseConcept" />
+    <node concept="PrWs8" id="3w0n0hzgWvI" role="PzmwI">
+      <ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
+    </node>
+    <node concept="1TJgyi" id="2AfSc6Jvjow" role="1TKVEl">
+      <property role="IQ2nx" value="2994859399702197792" />
+      <property role="TrG5h" value="description" />
+      <ref role="AX2Wp" to="tpck:fKAOsGN" resolve="string" />
+    </node>
+    <node concept="1TJgyj" id="$u9BK__SAr" role="1TKVEi">
+      <property role="IQ2ns" value="657004910291159451" />
+      <property role="20lmBu" value="aggregation" />
+      <property role="20kJfa" value="goal" />
+      <ref role="20lvS9" node="$u9BK__SA8" resolve="Goal" />
+    </node>
+    <node concept="1TJgyj" id="3JXBM6C4wQA" role="1TKVEi">
+      <property role="IQ2ns" value="4322786184248036774" />
+      <property role="20lmBu" value="aggregation" />
+      <property role="20kJfa" value="content" />
+      <property role="20lbJX" value="1..n" />
+      <ref role="20lvS9" node="3JXBM6C3UQB" resolve="Node" />
+    </node>
+    <node concept="PrWs8" id="3w0n0hzhVZC" role="PzmwI">
+      <ref role="PrY4T" node="3JXBM6C5urr" resolve="Root" />
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.propositional.mps b/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.propositional.mps
index baaebcfb..12de4b38 100644
--- a/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.propositional.mps
+++ b/samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.propositional.mps
@@ -22,6 +22,7 @@
       <concept id="4322786184247805399" name="jetbrains.mps.logic.propositional.structure.Not" flags="ng" index="2jWLFQ">
         <child id="4322786184247805400" name="target" index="2jWLFT" />
       </concept>
+      <concept id="4322786184247818020" name="jetbrains.mps.logic.propositional.structure.PropositionalProof" flags="ng" index="2jWMw5" />
       <concept id="4322786184247817766" name="jetbrains.mps.logic.propositional.structure.Or" flags="ng" index="2jWM$7">
         <child id="4322786184247817796" name="disjunct" index="2jWM__" />
       </concept>
@@ -45,11 +46,6 @@
       <concept id="4322786184247854968" name="jetbrains.mps.fitch.structure.Reasoning" flags="ng" index="2jWHxp">
         <child id="2497161927181071993" name="conclusion" index="3MT$nN" />
       </concept>
-      <concept id="4322786184247818020" name="jetbrains.mps.fitch.structure.Proof" flags="ng" index="2jWMw5">
-        <property id="2994859399702197792" name="description" index="26WHrx" />
-        <child id="4322786184248036774" name="content" index="2jVTa7" />
-        <child id="657004910291159451" name="goal" index="GyqZB" />
-      </concept>
       <concept id="4322786184247818022" name="jetbrains.mps.fitch.structure.Judgement" flags="ng" index="2jWMw7">
         <child id="4322786184247848320" name="premise" index="2jWFax" />
       </concept>
@@ -61,6 +57,11 @@
         <child id="657004910291159433" name="sentence" index="GyqZP" />
       </concept>
       <concept id="6123633795074140037" name="jetbrains.mps.fitch.structure.Reiteration" flags="ng" index="1l0MfV" />
+      <concept id="4035326440038975469" name="jetbrains.mps.fitch.structure.AbstractProof" flags="ng" index="1rgTJD">
+        <property id="2994859399702197792" name="description" index="26WHrx" />
+        <child id="4322786184248036774" name="content" index="2jVTa7" />
+        <child id="657004910291159451" name="goal" index="GyqZB" />
+      </concept>
     </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">
@@ -68,360 +69,420 @@
       </concept>
     </language>
   </registry>
-  <node concept="2jWMw5" id="3JXBM6C4h$e">
-    <property role="TrG5h" value="Tautology" />
-    <property role="26WHrx" value="Proove a tautology (p | ~p)" />
-    <node concept="2jWza5" id="$u9BK_y$0J" role="2jVTa7">
-      <node concept="2jWGsN" id="3JXBM6C4ztF" role="2jWza4">
-        <node concept="2jWLFQ" id="$u9BK_y$3a" role="3MT$nN">
-          <node concept="2jWM$7" id="3JXBM6C4ztG" role="2jWLFT">
-            <node concept="2jWLFD" id="3JXBM6C4ztH" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="5jVx7S2251s" role="2jWM__">
-              <node concept="2jWLFD" id="3JXBM6C4ztJ" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
-        </node>
+  <node concept="2jWMw5" id="2AfSc6Jv_cR">
+    <property role="TrG5h" value="Test1" />
+    <property role="26WHrx" value="Given p, q, and (p &amp; q =&gt; r) proove r." />
+    <node concept="GyqZO" id="2AfSc6Jv_cT" role="GyqZB">
+      <node concept="2jWLFD" id="2AfSc6Jv_cX" role="GyqZP">
+        <property role="TrG5h" value="r" />
       </node>
-      <node concept="2jWza5" id="3JXBM6Ca7o3" role="2jWza4">
-        <node concept="2jWGsN" id="3JXBM6Ca7o4" role="2jWza4">
-          <node concept="2jWLFD" id="3JXBM6Ca7o_" role="3MT$nN">
+    </node>
+    <node concept="GydIM" id="2AfSc6Jv_cZ" role="2jVTa7">
+      <node concept="2jWLFD" id="2AfSc6Jv_d4" role="3MT$nN">
+        <property role="TrG5h" value="p" />
+      </node>
+    </node>
+    <node concept="GydIM" id="2AfSc6Jv_da" role="2jVTa7">
+      <node concept="2jWLFD" id="2AfSc6Jv_dh" role="3MT$nN">
+        <property role="TrG5h" value="q" />
+      </node>
+    </node>
+    <node concept="GydIM" id="2AfSc6Jv_dp" role="2jVTa7">
+      <node concept="2jWM_K" id="2AfSc6Jv_dL" role="3MT$nN">
+        <node concept="2jWMFq" id="2AfSc6Jv_d_" role="2jWM_N">
+          <node concept="2jWLFD" id="2AfSc6Jv_dy" role="2jWMFt">
             <property role="TrG5h" value="p" />
           </node>
+          <node concept="2jWLFD" id="2AfSc6Jv_dG" role="2jWMFt">
+            <property role="TrG5h" value="q" />
+          </node>
         </node>
-        <node concept="2jWz55" id="3JXBM6Ca7oF" role="2jWza4">
-          <node concept="2jWMwi" id="3JXBM6Ca7p4" role="2jWFax">
-            <ref role="2jWMyc" node="3JXBM6Ca7o4" />
-          </node>
-          <node concept="2jWM$7" id="3JXBM6Ca7oS" role="3MT$nN">
-            <node concept="2jWLFD" id="3JXBM6Ca7oP" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="3JXBM6Ca7oZ" role="2jWM__">
-              <node concept="2jWLFD" id="3JXBM6Ca7p2" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
+        <node concept="2jWLFD" id="2AfSc6Jv_dW" role="2jWM_P">
+          <property role="TrG5h" value="r" />
         </node>
       </node>
-      <node concept="2jWAjC" id="3JXBM6Ca7pK" role="2jWza4">
-        <node concept="2jWMwi" id="2AfSc6JviTh" role="2jWFax">
-          <ref role="2jWMyc" node="3JXBM6Ca7o3" />
+    </node>
+    <node concept="2jWzbb" id="2AfSc6Jv_ea" role="2jVTa7">
+      <node concept="2jWMwi" id="2AfSc6Jv_es" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jv_cZ" />
+      </node>
+      <node concept="2jWMwi" id="2AfSc6Jv_ey" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jv_da" />
+      </node>
+      <node concept="2jWMFq" id="2AfSc6Jv_eD" role="3MT$nN">
+        <node concept="2jWLFD" id="2AfSc6Jv_eA" role="2jWMFt">
+          <property role="TrG5h" value="p" />
         </node>
-        <node concept="2jWM_K" id="3JXBM6Ca7qz" role="3MT$nN">
-          <node concept="2jWLFD" id="3JXBM6Ca7qv" role="2jWM_N">
-            <property role="TrG5h" value="p" />
-          </node>
-          <node concept="2jWM$7" id="3JXBM6Ca7qH" role="2jWM_P">
-            <node concept="2jWLFD" id="3JXBM6Ca7qE" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="3JXBM6Ca7qO" role="2jWM__">
-              <node concept="2jWLFD" id="3JXBM6Ca7qR" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
+        <node concept="2jWLFD" id="2AfSc6Jv_eK" role="2jWMFt">
+          <property role="TrG5h" value="q" />
         </node>
       </node>
-      <node concept="2jWza5" id="3JXBM6Ca7rP" role="2jWza4">
-        <node concept="2jWGsN" id="3JXBM6Ca7rQ" role="2jWza4">
-          <node concept="2jWLFD" id="3JXBM6Ca7sF" role="3MT$nN">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-        <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="5jVx7S21660" role="2jWM__">
-                <node concept="2jWLFD" id="5jVx7S21661" role="2jWLFT">
-                  <property role="TrG5h" value="p" />
-                </node>
-              </node>
-            </node>
-          </node>
-        </node>
+    </node>
+    <node concept="2jWAjR" id="2AfSc6JxVe6" role="2jVTa7">
+      <node concept="2jWMwi" id="2AfSc6JxVeu" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jv_dp" />
       </node>
-      <node concept="2jWAjC" id="$u9BK_yvcM" role="2jWza4">
-        <node concept="2jWM_K" id="$u9BK_yzWw" role="3MT$nN">
-          <node concept="2jWLFD" id="$u9BK_yzWs" role="2jWM_N">
-            <property role="TrG5h" value="p" />
-          </node>
-          <node concept="2jWLFQ" id="$u9BK_y$k$" role="2jWM_P">
-            <node concept="2jWM$7" id="$u9BK_yzWJ" role="2jWLFT">
-              <node concept="2jWLFD" id="$u9BK_yzWG" role="2jWM__">
-                <property role="TrG5h" value="p" />
-              </node>
-              <node concept="2jWLFQ" id="$u9BK_yzWQ" role="2jWM__">
-                <node concept="2jWLFD" id="$u9BK_yzWT" role="2jWLFT">
-                  <property role="TrG5h" value="p" />
-                </node>
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="2jWMwi" id="2AfSc6JviTv" role="2jWFax">
-          <ref role="2jWMyc" node="3JXBM6Ca7rP" />
-        </node>
+      <node concept="2jWMwi" id="2AfSc6JxVe$" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jv_ea" />
       </node>
-      <node concept="2jWz57" id="$u9BK_y$kO" role="2jWza4">
-        <node concept="2jWMwi" id="$u9BK_y$lO" role="2jWFax">
-          <ref role="2jWMyc" node="3JXBM6Ca7pK" />
+      <node concept="2jWLFD" id="2AfSc6JxVeC" role="3MT$nN">
+        <property role="TrG5h" value="r" />
+      </node>
+    </node>
+  </node>
+  <node concept="2jWMw5" id="3l440nVt5$e">
+    <property role="TrG5h" value="Nonsense" />
+    <property role="26WHrx" value="Ex nihilo quilibet. Proove nonsense given (p &amp; ~p)." />
+    <node concept="GyqZO" id="3l440nVt5$g" role="GyqZB">
+      <node concept="2jWLFD" id="3l440nVt5$k" role="GyqZP">
+        <property role="TrG5h" value="nonsense" />
+      </node>
+    </node>
+    <node concept="GydIM" id="1w94$GeTp5D" role="2jVTa7">
+      <node concept="2jWMFq" id="1w94$GeTp5T" role="3MT$nN">
+        <node concept="2jWLFD" id="1w94$GeTp5Q" role="2jWMFt">
+          <property role="TrG5h" value="p" />
         </node>
-        <node concept="2jWMwi" id="$u9BK_y$lU" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_yvcM" />
-        </node>
-        <node concept="2jWLFQ" id="$u9BK_y$lF" role="3MT$nN">
-          <node concept="2jWLFD" id="$u9BK_y$lJ" role="2jWLFT">
+        <node concept="2jWLFQ" id="1w94$GeTp60" role="2jWMFt">
+          <node concept="2jWLFD" id="1w94$GeTp63" role="2jWLFT">
             <property role="TrG5h" value="p" />
           </node>
         </node>
       </node>
     </node>
-    <node concept="2jWAjC" id="$u9BK_y$oJ" role="2jVTa7">
-      <node concept="2jWM_K" id="$u9BK_y$q$" role="3MT$nN">
-        <node concept="2jWLFQ" id="$u9BK_y$v0" role="2jWM_N">
-          <node concept="2jWM$7" id="$u9BK_y$qb" role="2jWLFT">
-            <node concept="2jWLFD" id="$u9BK_y$q8" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="$u9BK_y$qi" role="2jWM__">
-              <node concept="2jWLFD" id="$u9BK_y$ql" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="2jWLFQ" id="$u9BK_y$xn" role="2jWM_P">
-          <node concept="2jWLFD" id="$u9BK_y$xp" role="2jWLFT">
-            <property role="TrG5h" value="p" />
+    <node concept="2jWza5" id="1w94$GeTp6r" role="2jVTa7">
+      <node concept="2jWGsN" id="1w94$GeTp6s" role="2jWza4">
+        <node concept="2jWLFQ" id="1w94$GeTp6$" role="3MT$nN">
+          <node concept="2jWLFD" id="1w94$GeTp6A" role="2jWLFT">
+            <property role="TrG5h" value="nonsense" />
           </node>
         </node>
       </node>
-      <node concept="2jWMwi" id="2AfSc6JviTm" role="2jWFax">
-        <ref role="2jWMyc" node="$u9BK_y$0J" />
-      </node>
-    </node>
-    <node concept="2jWza5" id="$u9BK_y$yG" role="2jVTa7">
-      <node concept="2jWGsN" id="$u9BK_y$yH" role="2jWza4">
-        <node concept="2jWLFQ" id="$u9BK_y$yI" role="3MT$nN">
-          <node concept="2jWM$7" id="$u9BK_y$yJ" role="2jWLFT">
-            <node concept="2jWLFD" id="$u9BK_y$yK" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="$u9BK_y$yL" role="2jWM__">
-              <node concept="2jWLFD" id="$u9BK_y$yM" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
+      <node concept="2jWz52" id="1w94$GeTp71" role="2jWza4">
+        <node concept="2jWMwi" id="1w94$GeTp7c" role="2jWFax">
+          <ref role="2jWMyc" node="1w94$GeTp5D" />
         </node>
-      </node>
-      <node concept="2jWza5" id="$u9BK_y$yN" role="2jWza4">
-        <node concept="2jWGsN" id="$u9BK_y$yO" role="2jWza4">
-          <node concept="2jWLFQ" id="$u9BK_y$_m" role="3MT$nN">
-            <node concept="2jWLFD" id="$u9BK_y$yP" role="2jWLFT">
-              <property role="TrG5h" value="p" />
-            </node>
-          </node>
-        </node>
-        <node concept="2jWz55" id="$u9BK_y$yQ" role="2jWza4">
-          <node concept="2jWMwi" id="$u9BK_y$yR" role="2jWFax">
-            <ref role="2jWMyc" node="$u9BK_y$yO" />
-          </node>
-          <node concept="2jWM$7" id="$u9BK_y$yS" role="3MT$nN">
-            <node concept="2jWLFD" id="$u9BK_y$yT" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="$u9BK_y$yU" role="2jWM__">
-              <node concept="2jWLFD" id="$u9BK_y$yV" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
-        </node>
-      </node>
-      <node concept="2jWAjC" id="$u9BK_y$yW" role="2jWza4">
-        <node concept="2jWM_K" id="$u9BK_y$yZ" role="3MT$nN">
-          <node concept="2jWLFQ" id="$u9BK_y$_r" role="2jWM_N">
-            <node concept="2jWLFD" id="$u9BK_y$z0" role="2jWLFT">
-              <property role="TrG5h" value="p" />
-            </node>
-          </node>
-          <node concept="2jWM$7" id="$u9BK_y$z1" role="2jWM_P">
-            <node concept="2jWLFD" id="$u9BK_y$z2" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="$u9BK_y$z3" role="2jWM__">
-              <node concept="2jWLFD" id="$u9BK_y$z4" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="2jWMwi" id="2AfSc6JviTo" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$yN" />
-        </node>
-      </node>
-      <node concept="2jWza5" id="$u9BK_y$z5" role="2jWza4">
-        <node concept="2jWGsN" id="$u9BK_y$z6" role="2jWza4">
-          <node concept="2jWLFQ" id="$u9BK_y$_w" role="3MT$nN">
-            <node concept="2jWLFD" id="$u9BK_y$z7" role="2jWLFT">
-              <property role="TrG5h" value="p" />
-            </node>
-          </node>
-        </node>
-        <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="5jVx7S22tDl" role="2jWM__">
-                <node concept="2jWLFD" id="5jVx7S22tDm" role="2jWLFT">
-                  <property role="TrG5h" value="p" />
-                </node>
-              </node>
-            </node>
-          </node>
-        </node>
-      </node>
-      <node concept="2jWAjC" id="$u9BK_y$ze" role="2jWza4">
-        <node concept="2jWM_K" id="$u9BK_y$zh" role="3MT$nN">
-          <node concept="2jWLFQ" id="$u9BK_y$__" role="2jWM_N">
-            <node concept="2jWLFD" id="$u9BK_y$zi" role="2jWLFT">
-              <property role="TrG5h" value="p" />
-            </node>
-          </node>
-          <node concept="2jWLFQ" id="$u9BK_y$zj" role="2jWM_P">
-            <node concept="2jWM$7" id="$u9BK_y$zk" role="2jWLFT">
-              <node concept="2jWLFD" id="$u9BK_y$zl" role="2jWM__">
-                <property role="TrG5h" value="p" />
-              </node>
-              <node concept="2jWLFQ" id="$u9BK_y$zm" role="2jWM__">
-                <node concept="2jWLFD" id="$u9BK_y$zn" role="2jWLFT">
-                  <property role="TrG5h" value="p" />
-                </node>
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="2jWMwi" id="2AfSc6JviTq" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$z5" />
-        </node>
-      </node>
-      <node concept="2jWz57" id="$u9BK_y$zo" role="2jWza4">
-        <node concept="2jWMwi" id="$u9BK_y$zp" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$yW" />
-        </node>
-        <node concept="2jWMwi" id="$u9BK_y$zq" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$ze" />
-        </node>
-        <node concept="2jWLFQ" id="$u9BK_y$zr" role="3MT$nN">
-          <node concept="2jWLFQ" id="$u9BK_y$_E" role="2jWLFT">
-            <node concept="2jWLFD" id="$u9BK_y$zs" role="2jWLFT">
-              <property role="TrG5h" value="p" />
-            </node>
-          </node>
-        </node>
-      </node>
-      <node concept="2jWAjD" id="$u9BK_y$A_" role="2jWza4">
-        <node concept="2jWMwi" id="$u9BK_y$B$" role="2jWFax">
-          <ref role="2jWMyc" node="$u9BK_y$zo" />
-        </node>
-        <node concept="2jWLFD" id="$u9BK_y$By" role="3MT$nN">
+        <node concept="2jWLFD" id="1w94$GeTp7f" role="3MT$nN">
           <property role="TrG5h" value="p" />
         </node>
       </node>
     </node>
-    <node concept="2jWAjC" id="$u9BK_y$yx" role="2jVTa7">
-      <node concept="2jWM_K" id="$u9BK_y$y$" role="3MT$nN">
-        <node concept="2jWLFQ" id="$u9BK_y$yB" role="2jWM_N">
-          <node concept="2jWM$7" id="$u9BK_y$yC" role="2jWLFT">
-            <node concept="2jWLFD" id="$u9BK_y$yD" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="$u9BK_y$yE" role="2jWM__">
-              <node concept="2jWLFD" id="$u9BK_y$yF" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
+    <node concept="2jWAjC" id="1w94$GeTp7G" role="2jVTa7">
+      <node concept="2jWMwi" id="1w94$GeTp80" role="2jWFax">
+        <ref role="2jWMyc" node="1w94$GeTp6r" />
+      </node>
+      <node concept="2jWM_K" id="1w94$GeTp89" role="3MT$nN">
+        <node concept="2jWLFQ" id="1w94$GeTp8j" role="2jWM_N">
+          <node concept="2jWLFD" id="1w94$GeTp85" role="2jWLFT">
+            <property role="TrG5h" value="nonsense" />
           </node>
         </node>
-        <node concept="2jWLFD" id="$u9BK_y$yA" role="2jWM_P">
+        <node concept="2jWLFD" id="1w94$GeTp8g" role="2jWM_P">
           <property role="TrG5h" value="p" />
         </node>
       </node>
-      <node concept="2jWMwi" id="2AfSc6JviTz" role="2jWFax">
-        <ref role="2jWMyc" node="$u9BK_y$yG" />
-      </node>
     </node>
-    <node concept="2jWz57" id="$u9BK_y$DL" role="2jVTa7">
-      <node concept="2jWMwi" id="$u9BK_y$Gw" role="2jWFax">
-        <ref role="2jWMyc" node="$u9BK_y$oJ" />
-      </node>
-      <node concept="2jWMwi" id="$u9BK_y$G_" role="2jWFax">
-        <ref role="2jWMyc" node="$u9BK_y$yx" />
-      </node>
-      <node concept="2jWLFQ" id="$u9BK_y$G8" role="3MT$nN">
-        <node concept="2jWLFQ" id="$u9BK_y$Gj" role="2jWLFT">
-          <node concept="2jWM$7" id="$u9BK_y$FV" role="2jWLFT">
-            <node concept="2jWLFD" id="$u9BK_y$FS" role="2jWM__">
-              <property role="TrG5h" value="p" />
-            </node>
-            <node concept="2jWLFQ" id="$u9BK_y$G2" role="2jWM__">
-              <node concept="2jWLFD" id="$u9BK_y$G5" role="2jWLFT">
-                <property role="TrG5h" value="p" />
-              </node>
-            </node>
+    <node concept="2jWza5" id="1w94$GeTp8J" role="2jVTa7">
+      <node concept="2jWGsN" id="1w94$GeTp8K" role="2jWza4">
+        <node concept="2jWLFQ" id="1w94$GeTp95" role="3MT$nN">
+          <node concept="2jWLFD" id="1w94$GeTp97" role="2jWLFT">
+            <property role="TrG5h" value="nonsense" />
           </node>
         </node>
       </node>
-    </node>
-    <node concept="2jWAjD" id="$u9BK_y$IN" role="2jVTa7">
-      <node concept="2jWMwi" id="$u9BK_y$Li" role="2jWFax">
-        <ref role="2jWMyc" node="$u9BK_y$DL" />
-      </node>
-      <node concept="2jWM$7" id="$u9BK_y$L6" role="3MT$nN">
-        <node concept="2jWLFD" id="$u9BK_y$L3" role="2jWM__">
-          <property role="TrG5h" value="p" />
+      <node concept="2jWz52" id="1w94$GeTp9e" role="2jWza4">
+        <node concept="2jWMwi" id="1w94$GeTp9p" role="2jWFax">
+          <ref role="2jWMyc" node="1w94$GeTp5D" />
         </node>
-        <node concept="2jWLFQ" id="$u9BK_y$Ld" role="2jWM__">
-          <node concept="2jWLFD" id="$u9BK_y$Lg" role="2jWLFT">
+        <node concept="2jWLFQ" id="1w94$GeTp9s" role="3MT$nN">
+          <node concept="2jWLFD" id="1w94$GeTp9u" role="2jWLFT">
             <property role="TrG5h" value="p" />
           </node>
         </node>
       </node>
     </node>
-    <node concept="GyqZO" id="$u9BK_AaA7" role="GyqZB">
-      <node concept="2jWM$7" id="$u9BK_AaAe" role="GyqZP">
-        <node concept="2jWLFD" id="$u9BK_AaAb" role="2jWM__">
-          <property role="TrG5h" value="p" />
+    <node concept="2jWAjC" id="1w94$GeTpab" role="2jVTa7">
+      <node concept="2jWMwi" id="1w94$GeTpaH" role="2jWFax">
+        <ref role="2jWMyc" node="1w94$GeTp8J" />
+      </node>
+      <node concept="2jWM_K" id="1w94$GeTpaO" role="3MT$nN">
+        <node concept="2jWLFQ" id="1w94$GeTpb0" role="2jWM_N">
+          <node concept="2jWLFD" id="1w94$GeTpaK" role="2jWLFT">
+            <property role="TrG5h" value="nonsense" />
+          </node>
         </node>
-        <node concept="2jWLFQ" id="$u9BK_AaAl" role="2jWM__">
-          <node concept="2jWLFD" id="$u9BK_AaAo" role="2jWLFT">
+        <node concept="2jWLFQ" id="1w94$GeTpaV" role="2jWM_P">
+          <node concept="2jWLFD" id="1w94$GeTpaX" role="2jWLFT">
             <property role="TrG5h" value="p" />
           </node>
         </node>
       </node>
     </node>
+    <node concept="2jWz57" id="1w94$GeTpbB" role="2jVTa7">
+      <node concept="2jWMwi" id="1w94$GeTpcg" role="2jWFax">
+        <ref role="2jWMyc" node="1w94$GeTp7G" />
+      </node>
+      <node concept="2jWMwi" id="1w94$GeTpcm" role="2jWFax">
+        <ref role="2jWMyc" node="1w94$GeTpab" />
+      </node>
+      <node concept="2jWLFQ" id="1w94$GeTpcq" role="3MT$nN">
+        <node concept="2jWLFQ" id="1w94$GeTpcs" role="2jWLFT">
+          <node concept="2jWLFD" id="1w94$GeTpcu" role="2jWLFT">
+            <property role="TrG5h" value="nonsense" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjD" id="1w94$GeTpd9" role="2jVTa7">
+      <node concept="2jWMwi" id="1w94$GeTpdS" role="2jWFax">
+        <ref role="2jWMyc" node="1w94$GeTpbB" />
+      </node>
+      <node concept="2jWLFD" id="1w94$GeTpdV" role="3MT$nN">
+        <property role="TrG5h" value="nonsense" />
+      </node>
+    </node>
+  </node>
+  <node concept="2jWMw5" id="2AfSc6Jv$28">
+    <property role="TrG5h" value="Contrapositive" />
+    <property role="26WHrx" value="Proove the contrapositive (~q =&gt; ~p) given (p =&gt; q)" />
+    <node concept="GyqZO" id="2AfSc6Jv$2a" role="GyqZB">
+      <node concept="2jWM_K" id="2AfSc6Jv$2k" role="GyqZP">
+        <node concept="2jWLFQ" id="2AfSc6Jv$2z" role="2jWM_N">
+          <node concept="2jWLFD" id="2AfSc6Jv$2e" role="2jWLFT">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+        <node concept="2jWLFQ" id="2AfSc6Jv$2u" role="2jWM_P">
+          <node concept="2jWLFD" id="2AfSc6Jv$2r" role="2jWLFT">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="GydIM" id="2AfSc6Jv$2B" role="2jVTa7">
+      <node concept="2jWM_K" id="2AfSc6Jv$2K" role="3MT$nN">
+        <node concept="2jWLFD" id="2AfSc6Jv$2G" role="2jWM_N">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFD" id="2AfSc6Jv$2R" role="2jWM_P">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWza5" id="2AfSc6Jv$2Z" role="2jVTa7">
+      <node concept="2jWGsN" id="2AfSc6Jv$30" role="2jWza4">
+        <node concept="2jWLFQ" id="2AfSc6Jv$37" role="3MT$nN">
+          <node concept="2jWLFD" id="2AfSc6Jv$39" role="2jWLFT">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+      </node>
+      <node concept="2jWza5" id="2AfSc6Jv$3g" role="2jWza4">
+        <node concept="2jWGsN" id="2AfSc6Jv$3h" role="2jWza4">
+          <node concept="2jWLFD" id="2AfSc6Jv$3n" role="3MT$nN">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+        <node concept="1l0MfV" id="2AfSc6Jv$3t" role="2jWza4">
+          <node concept="2jWMwi" id="2AfSc6Jv$3u" role="2jWFax">
+            <ref role="2jWMyc" node="2AfSc6Jv$30" />
+          </node>
+          <node concept="2jWLFQ" id="2AfSc6Jv$3v" role="3MT$nN">
+            <node concept="2jWLFD" id="2AfSc6Jv$3w" role="2jWLFT">
+              <property role="TrG5h" value="q" />
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2jWAjC" id="2AfSc6Jv$4_" role="2jWza4">
+        <node concept="2jWMwi" id="2AfSc6Jv$4R" role="2jWFax">
+          <ref role="2jWMyc" node="2AfSc6Jv$3g" />
+        </node>
+        <node concept="2jWM_K" id="2AfSc6Jv$4Y" role="3MT$nN">
+          <node concept="2jWLFD" id="2AfSc6Jv$4U" role="2jWM_N">
+            <property role="TrG5h" value="p" />
+          </node>
+          <node concept="2jWLFQ" id="2AfSc6Jv$58" role="2jWM_P">
+            <node concept="2jWLFD" id="2AfSc6Jv$55" role="2jWLFT">
+              <property role="TrG5h" value="q" />
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2jWza5" id="2AfSc6Jv$5u" role="2jWza4">
+        <node concept="2jWGsN" id="2AfSc6Jv$5v" role="2jWza4">
+          <node concept="2jWLFD" id="2AfSc6Jv$5M" role="3MT$nN">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+        <node concept="2jWAjR" id="2AfSc6Jv$5S" role="2jWza4">
+          <node concept="2jWMwi" id="2AfSc6Jv$62" role="2jWFax">
+            <ref role="2jWMyc" node="2AfSc6Jv$2B" />
+          </node>
+          <node concept="2jWMwi" id="2AfSc6Jv$68" role="2jWFax">
+            <ref role="2jWMyc" node="2AfSc6Jv$5v" />
+          </node>
+          <node concept="2jWLFD" id="2AfSc6Jv$6c" role="3MT$nN">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+      </node>
+      <node concept="2jWAjC" id="2AfSc6Jv$6O" role="2jWza4">
+        <node concept="2jWMwi" id="2AfSc6Jv$7j" role="2jWFax">
+          <ref role="2jWMyc" node="2AfSc6Jv$5u" />
+        </node>
+        <node concept="2jWM_K" id="2AfSc6Jv$7q" role="3MT$nN">
+          <node concept="2jWLFD" id="2AfSc6Jv$7m" role="2jWM_N">
+            <property role="TrG5h" value="p" />
+          </node>
+          <node concept="2jWLFD" id="2AfSc6Jv$7x" role="2jWM_P">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+      </node>
+      <node concept="2jWz57" id="2AfSc6Jv$86" role="2jWza4">
+        <node concept="2jWMwi" id="2AfSc6Jv$9U" role="2jWFax">
+          <ref role="2jWMyc" node="2AfSc6Jv$4_" />
+        </node>
+        <node concept="2jWMwi" id="2AfSc6Jv$a0" role="2jWFax">
+          <ref role="2jWMyc" node="2AfSc6Jv$6O" />
+        </node>
+        <node concept="2jWLFQ" id="2AfSc6Jv$a4" role="3MT$nN">
+          <node concept="2jWLFD" id="2AfSc6Jv$a6" role="2jWLFT">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjC" id="2AfSc6Jv$aL" role="2jVTa7">
+      <node concept="2jWMwi" id="2AfSc6Jv$bv" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jv$2Z" />
+      </node>
+      <node concept="2jWM_K" id="2AfSc6Jv$bE" role="3MT$nN">
+        <node concept="2jWLFQ" id="2AfSc6Jv$bT" role="2jWM_N">
+          <node concept="2jWLFD" id="2AfSc6Jv$bA" role="2jWLFT">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+        <node concept="2jWLFQ" id="2AfSc6Jv$bO" role="2jWM_P">
+          <node concept="2jWLFD" id="2AfSc6Jv$bL" role="2jWLFT">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+      </node>
+    </node>
+  </node>
+  <node concept="2jWMw5" id="3l440nVrsN1">
+    <property role="TrG5h" value="Test5" />
+    <property role="26WHrx" value="Given (p &amp; q) proove (p &lt;=&gt; q)" />
+    <node concept="GyqZO" id="3l440nVrsN3" role="GyqZB">
+      <node concept="2jWMB0" id="3l440nVrsNb" role="GyqZP">
+        <node concept="2jWLFD" id="3l440nVrsN7" role="2jWMBa">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrsNi" role="2jWMBd">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
+    <node concept="GydIM" id="3l440nVrsNk" role="2jVTa7">
+      <node concept="2jWMFq" id="3l440nVrsNJ" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVrsNp" role="2jWMFt">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrsNQ" role="2jWMFt">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWza5" id="3l440nVrsOD" role="2jVTa7">
+      <node concept="2jWGsN" id="3l440nVrsOE" role="2jWza4">
+        <node concept="2jWLFD" id="3l440nVrsOR" role="3MT$nN">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+      <node concept="2jWz52" id="3l440nVrsOf" role="2jWza4">
+        <node concept="2jWMwi" id="3l440nVrsOg" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVrsNk" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrsOh" role="3MT$nN">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjC" id="3l440nVrzqG" role="2jVTa7">
+      <node concept="2jWMwi" id="3l440nVrzr1" role="2jWFax">
+        <ref role="2jWMyc" node="3l440nVrsOD" />
+      </node>
+      <node concept="2jWM_K" id="3l440nVrzr8" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVrzr4" role="2jWM_N">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrzrf" role="2jWM_P">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWza5" id="3l440nVrzr_" role="2jVTa7">
+      <node concept="2jWGsN" id="3l440nVrzrA" role="2jWza4">
+        <node concept="2jWLFD" id="3l440nVrzrV" role="3MT$nN">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+      <node concept="2jWz52" id="3l440nVrsNY" role="2jWza4">
+        <node concept="2jWMwi" id="3l440nVrsOa" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVrsNk" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrsOd" role="3MT$nN">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjC" id="3l440nVrzuf" role="2jVTa7">
+      <node concept="2jWMwi" id="3l440nVrzuG" role="2jWFax">
+        <ref role="2jWMyc" node="3l440nVrzr_" />
+      </node>
+      <node concept="2jWM_K" id="3l440nVrzuN" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVrzuJ" role="2jWM_N">
+          <property role="TrG5h" value="q" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrzuU" role="2jWM_P">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjQ" id="3l440nVrzvo" role="2jVTa7">
+      <node concept="2jWMwi" id="3l440nVrzvU" role="2jWFax">
+        <ref role="2jWMyc" node="3l440nVrzqG" />
+      </node>
+      <node concept="2jWMwi" id="3l440nVrzw0" role="2jWFax">
+        <ref role="2jWMyc" node="3l440nVrzuf" />
+      </node>
+      <node concept="2jWMB0" id="3l440nVrzwa" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVrzw4" role="2jWMBa">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVrzwh" role="2jWMBd">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
   </node>
   <node concept="2jWMw5" id="5jVx7S230hl">
     <property role="TrG5h" value="Implication" />
     <property role="26WHrx" value="Proove alternative form of implication (~p | q) given (p =&gt; q)" />
+    <node concept="GyqZO" id="5jVx7S230kM" role="GyqZB">
+      <node concept="2jWM$7" id="5jVx7S230lc" role="GyqZP">
+        <node concept="2jWLFQ" id="5jVx7S230ln" role="2jWM__">
+          <node concept="2jWLFD" id="5jVx7S230l9" role="2jWLFT">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+        <node concept="2jWLFD" id="5jVx7S230lj" role="2jWM__">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
     <node concept="GydIM" id="5jVx7S230ls" role="2jVTa7">
       <node concept="2jWM_K" id="5jVx7S230l_" role="3MT$nN">
         <node concept="2jWLFD" id="5jVx7S230lx" role="2jWM_N">
@@ -778,250 +839,91 @@
         </node>
       </node>
     </node>
-    <node concept="GyqZO" id="5jVx7S230kM" role="GyqZB">
-      <node concept="2jWM$7" id="5jVx7S230lc" role="GyqZP">
-        <node concept="2jWLFQ" id="5jVx7S230ln" role="2jWM__">
-          <node concept="2jWLFD" id="5jVx7S230l9" role="2jWLFT">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-        <node concept="2jWLFD" id="5jVx7S230lj" role="2jWM__">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
   </node>
-  <node concept="2jWMw5" id="2AfSc6Jv$28">
-    <property role="TrG5h" value="Contrapositive" />
-    <property role="26WHrx" value="Proove the contrapositive (~q =&gt; ~p) given (p =&gt; q)" />
-    <node concept="GydIM" id="2AfSc6Jv$2B" role="2jVTa7">
-      <node concept="2jWM_K" id="2AfSc6Jv$2K" role="3MT$nN">
-        <node concept="2jWLFD" id="2AfSc6Jv$2G" role="2jWM_N">
+  <node concept="2jWMw5" id="3l440nVqpsF">
+    <property role="TrG5h" value="Test4" />
+    <property role="26WHrx" value="Given (p =&gt; q) and (q &lt;=&gt; r) proove (p =&gt; r)" />
+    <node concept="GyqZO" id="3l440nVqpsH" role="GyqZB">
+      <node concept="2jWM_K" id="3l440nVqpsP" role="GyqZP">
+        <node concept="2jWLFD" id="3l440nVqpsL" role="2jWM_N">
           <property role="TrG5h" value="p" />
         </node>
-        <node concept="2jWLFD" id="2AfSc6Jv$2R" role="2jWM_P">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWza5" id="2AfSc6Jv$2Z" role="2jVTa7">
-      <node concept="2jWGsN" id="2AfSc6Jv$30" role="2jWza4">
-        <node concept="2jWLFQ" id="2AfSc6Jv$37" role="3MT$nN">
-          <node concept="2jWLFD" id="2AfSc6Jv$39" role="2jWLFT">
-            <property role="TrG5h" value="q" />
-          </node>
-        </node>
-      </node>
-      <node concept="2jWza5" id="2AfSc6Jv$3g" role="2jWza4">
-        <node concept="2jWGsN" id="2AfSc6Jv$3h" role="2jWza4">
-          <node concept="2jWLFD" id="2AfSc6Jv$3n" role="3MT$nN">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-        <node concept="1l0MfV" id="2AfSc6Jv$3t" role="2jWza4">
-          <node concept="2jWMwi" id="2AfSc6Jv$3u" role="2jWFax">
-            <ref role="2jWMyc" node="2AfSc6Jv$30" />
-          </node>
-          <node concept="2jWLFQ" id="2AfSc6Jv$3v" role="3MT$nN">
-            <node concept="2jWLFD" id="2AfSc6Jv$3w" role="2jWLFT">
-              <property role="TrG5h" value="q" />
-            </node>
-          </node>
-        </node>
-      </node>
-      <node concept="2jWAjC" id="2AfSc6Jv$4_" role="2jWza4">
-        <node concept="2jWMwi" id="2AfSc6Jv$4R" role="2jWFax">
-          <ref role="2jWMyc" node="2AfSc6Jv$3g" />
-        </node>
-        <node concept="2jWM_K" id="2AfSc6Jv$4Y" role="3MT$nN">
-          <node concept="2jWLFD" id="2AfSc6Jv$4U" role="2jWM_N">
-            <property role="TrG5h" value="p" />
-          </node>
-          <node concept="2jWLFQ" id="2AfSc6Jv$58" role="2jWM_P">
-            <node concept="2jWLFD" id="2AfSc6Jv$55" role="2jWLFT">
-              <property role="TrG5h" value="q" />
-            </node>
-          </node>
-        </node>
-      </node>
-      <node concept="2jWza5" id="2AfSc6Jv$5u" role="2jWza4">
-        <node concept="2jWGsN" id="2AfSc6Jv$5v" role="2jWza4">
-          <node concept="2jWLFD" id="2AfSc6Jv$5M" role="3MT$nN">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-        <node concept="2jWAjR" id="2AfSc6Jv$5S" role="2jWza4">
-          <node concept="2jWMwi" id="2AfSc6Jv$62" role="2jWFax">
-            <ref role="2jWMyc" node="2AfSc6Jv$2B" />
-          </node>
-          <node concept="2jWMwi" id="2AfSc6Jv$68" role="2jWFax">
-            <ref role="2jWMyc" node="2AfSc6Jv$5v" />
-          </node>
-          <node concept="2jWLFD" id="2AfSc6Jv$6c" role="3MT$nN">
-            <property role="TrG5h" value="q" />
-          </node>
-        </node>
-      </node>
-      <node concept="2jWAjC" id="2AfSc6Jv$6O" role="2jWza4">
-        <node concept="2jWMwi" id="2AfSc6Jv$7j" role="2jWFax">
-          <ref role="2jWMyc" node="2AfSc6Jv$5u" />
-        </node>
-        <node concept="2jWM_K" id="2AfSc6Jv$7q" role="3MT$nN">
-          <node concept="2jWLFD" id="2AfSc6Jv$7m" role="2jWM_N">
-            <property role="TrG5h" value="p" />
-          </node>
-          <node concept="2jWLFD" id="2AfSc6Jv$7x" role="2jWM_P">
-            <property role="TrG5h" value="q" />
-          </node>
-        </node>
-      </node>
-      <node concept="2jWz57" id="2AfSc6Jv$86" role="2jWza4">
-        <node concept="2jWMwi" id="2AfSc6Jv$9U" role="2jWFax">
-          <ref role="2jWMyc" node="2AfSc6Jv$4_" />
-        </node>
-        <node concept="2jWMwi" id="2AfSc6Jv$a0" role="2jWFax">
-          <ref role="2jWMyc" node="2AfSc6Jv$6O" />
-        </node>
-        <node concept="2jWLFQ" id="2AfSc6Jv$a4" role="3MT$nN">
-          <node concept="2jWLFD" id="2AfSc6Jv$a6" role="2jWLFT">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-      </node>
-    </node>
-    <node concept="2jWAjC" id="2AfSc6Jv$aL" role="2jVTa7">
-      <node concept="2jWMwi" id="2AfSc6Jv$bv" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jv$2Z" />
-      </node>
-      <node concept="2jWM_K" id="2AfSc6Jv$bE" role="3MT$nN">
-        <node concept="2jWLFQ" id="2AfSc6Jv$bT" role="2jWM_N">
-          <node concept="2jWLFD" id="2AfSc6Jv$bA" role="2jWLFT">
-            <property role="TrG5h" value="q" />
-          </node>
-        </node>
-        <node concept="2jWLFQ" id="2AfSc6Jv$bO" role="2jWM_P">
-          <node concept="2jWLFD" id="2AfSc6Jv$bL" role="2jWLFT">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-      </node>
-    </node>
-    <node concept="GyqZO" id="2AfSc6Jv$2a" role="GyqZB">
-      <node concept="2jWM_K" id="2AfSc6Jv$2k" role="GyqZP">
-        <node concept="2jWLFQ" id="2AfSc6Jv$2z" role="2jWM_N">
-          <node concept="2jWLFD" id="2AfSc6Jv$2e" role="2jWLFT">
-            <property role="TrG5h" value="q" />
-          </node>
-        </node>
-        <node concept="2jWLFQ" id="2AfSc6Jv$2u" role="2jWM_P">
-          <node concept="2jWLFD" id="2AfSc6Jv$2r" role="2jWLFT">
-            <property role="TrG5h" value="p" />
-          </node>
-        </node>
-      </node>
-    </node>
-  </node>
-  <node concept="2jWMw5" id="2AfSc6Jv_cR">
-    <property role="TrG5h" value="Test1" />
-    <property role="26WHrx" value="Given p, q, and (p &amp; q =&gt; r) proove r." />
-    <node concept="GydIM" id="2AfSc6Jv_cZ" role="2jVTa7">
-      <node concept="2jWLFD" id="2AfSc6Jv_d4" role="3MT$nN">
-        <property role="TrG5h" value="p" />
-      </node>
-    </node>
-    <node concept="GydIM" id="2AfSc6Jv_da" role="2jVTa7">
-      <node concept="2jWLFD" id="2AfSc6Jv_dh" role="3MT$nN">
-        <property role="TrG5h" value="q" />
-      </node>
-    </node>
-    <node concept="GydIM" id="2AfSc6Jv_dp" role="2jVTa7">
-      <node concept="2jWM_K" id="2AfSc6Jv_dL" role="3MT$nN">
-        <node concept="2jWMFq" id="2AfSc6Jv_d_" role="2jWM_N">
-          <node concept="2jWLFD" id="2AfSc6Jv_dy" role="2jWMFt">
-            <property role="TrG5h" value="p" />
-          </node>
-          <node concept="2jWLFD" id="2AfSc6Jv_dG" role="2jWMFt">
-            <property role="TrG5h" value="q" />
-          </node>
-        </node>
-        <node concept="2jWLFD" id="2AfSc6Jv_dW" role="2jWM_P">
+        <node concept="2jWLFD" id="3l440nVqpsW" role="2jWM_P">
           <property role="TrG5h" value="r" />
         </node>
       </node>
     </node>
-    <node concept="2jWzbb" id="2AfSc6Jv_ea" role="2jVTa7">
-      <node concept="2jWMwi" id="2AfSc6Jv_es" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jv_cZ" />
-      </node>
-      <node concept="2jWMwi" id="2AfSc6Jv_ey" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jv_da" />
-      </node>
-      <node concept="2jWMFq" id="2AfSc6Jv_eD" role="3MT$nN">
-        <node concept="2jWLFD" id="2AfSc6Jv_eA" role="2jWMFt">
+    <node concept="GydIM" id="3l440nVqpsY" role="2jVTa7">
+      <node concept="2jWM_K" id="3l440nVqpt7" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVqpt3" role="2jWM_N">
           <property role="TrG5h" value="p" />
         </node>
-        <node concept="2jWLFD" id="2AfSc6Jv_eK" role="2jWMFt">
+        <node concept="2jWLFD" id="3l440nVqpte" role="2jWM_P">
           <property role="TrG5h" value="q" />
         </node>
       </node>
     </node>
-    <node concept="2jWAjR" id="2AfSc6JxVe6" role="2jVTa7">
-      <node concept="2jWMwi" id="2AfSc6JxVeu" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jv_dp" />
-      </node>
-      <node concept="2jWMwi" id="2AfSc6JxVe$" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jv_ea" />
-      </node>
-      <node concept="2jWLFD" id="2AfSc6JxVeC" role="3MT$nN">
-        <property role="TrG5h" value="r" />
-      </node>
-    </node>
-    <node concept="GyqZO" id="2AfSc6Jv_cT" role="GyqZB">
-      <node concept="2jWLFD" id="2AfSc6Jv_cX" role="GyqZP">
-        <property role="TrG5h" value="r" />
-      </node>
-    </node>
-  </node>
-  <node concept="2jWMw5" id="2AfSc6Jw7pl">
-    <property role="TrG5h" value="Test2" />
-    <property role="26WHrx" value="Given (p &amp; q) prove (q | r)" />
-    <node concept="GydIM" id="2AfSc6Jw7pC" role="2jVTa7">
-      <node concept="2jWMFq" id="2AfSc6Jw7pK" role="3MT$nN">
-        <node concept="2jWLFD" id="2AfSc6Jw7pH" role="2jWMFt">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFD" id="2AfSc6Jw7pR" role="2jWMFt">
+    <node concept="GydIM" id="3l440nVqptm" role="2jVTa7">
+      <node concept="2jWMB0" id="3l440nVqptB" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVqptv" role="2jWMBa">
           <property role="TrG5h" value="q" />
         </node>
-      </node>
-    </node>
-    <node concept="2jWz52" id="2AfSc6Jw7q0" role="2jVTa7">
-      <node concept="2jWMwi" id="2AfSc6Jw7qc" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jw7pC" />
-      </node>
-      <node concept="2jWLFD" id="2AfSc6Jw7qf" role="3MT$nN">
-        <property role="TrG5h" value="q" />
-      </node>
-    </node>
-    <node concept="2jWz55" id="2AfSc6JxVdj" role="2jVTa7">
-      <node concept="2jWMwi" id="2AfSc6JxVdy" role="2jWFax">
-        <ref role="2jWMyc" node="2AfSc6Jw7q0" />
-      </node>
-      <node concept="2jWM$7" id="2AfSc6JxVdC" role="3MT$nN">
-        <node concept="2jWLFD" id="2AfSc6JxVd_" role="2jWM__">
-          <property role="TrG5h" value="q" />
-        </node>
-        <node concept="2jWLFD" id="2AfSc6JxVdJ" role="2jWM__">
+        <node concept="2jWLFD" id="3l440nVqptI" role="2jWMBd">
           <property role="TrG5h" value="r" />
         </node>
       </node>
     </node>
-    <node concept="GyqZO" id="2AfSc6Jw7pn" role="GyqZB">
-      <node concept="2jWM$7" id="2AfSc6Jw7pu" role="GyqZP">
-        <node concept="2jWLFD" id="2AfSc6Jw7pr" role="2jWM__">
+    <node concept="2jWza5" id="3l440nVqptU" role="2jVTa7">
+      <node concept="2jWGsN" id="3l440nVqptV" role="2jWza4">
+        <node concept="2jWLFD" id="3l440nVqpu6" role="3MT$nN">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+      <node concept="2jWAjR" id="3l440nVqpuc" role="2jWza4">
+        <node concept="2jWMwi" id="3l440nVqpum" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVqpsY" />
+        </node>
+        <node concept="2jWMwi" id="3l440nVqpus" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVqptV" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVqpuw" role="3MT$nN">
           <property role="TrG5h" value="q" />
         </node>
-        <node concept="2jWLFD" id="2AfSc6Jw7p_" role="2jWM__">
+      </node>
+      <node concept="2jWAjT" id="3l440nVqpuF" role="2jWza4">
+        <node concept="2jWMwi" id="3l440nVqpuT" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVqptm" />
+        </node>
+        <node concept="2jWM_K" id="3l440nVqpv0" role="3MT$nN">
+          <node concept="2jWLFD" id="3l440nVqpuW" role="2jWM_N">
+            <property role="TrG5h" value="q" />
+          </node>
+          <node concept="2jWLFD" id="3l440nVqpv7" role="2jWM_P">
+            <property role="TrG5h" value="r" />
+          </node>
+        </node>
+      </node>
+      <node concept="2jWAjR" id="3l440nVr59R" role="2jWza4">
+        <node concept="2jWMwi" id="3l440nVr5aa" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVqpuF" />
+        </node>
+        <node concept="2jWMwi" id="3l440nVr5ag" role="2jWFax">
+          <ref role="2jWMyc" node="3l440nVqpuc" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVr5ak" role="3MT$nN">
+          <property role="TrG5h" value="r" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjC" id="3l440nVr5bg" role="2jVTa7">
+      <node concept="2jWMwi" id="3l440nVr5bK" role="2jWFax">
+        <ref role="2jWMyc" node="3l440nVqptU" />
+      </node>
+      <node concept="2jWM_K" id="3l440nVr5bR" role="3MT$nN">
+        <node concept="2jWLFD" id="3l440nVr5bN" role="2jWM_N">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFD" id="3l440nVr5bY" role="2jWM_P">
           <property role="TrG5h" value="r" />
         </node>
       </node>
@@ -1030,6 +932,16 @@
   <node concept="2jWMw5" id="2AfSc6JxXEN">
     <property role="TrG5h" value="Test3" />
     <property role="26WHrx" value="Given (p =&gt; q) and (m =&gt; (p | q)) proove (m =&gt; q)" />
+    <node concept="GyqZO" id="2AfSc6JxXET" role="GyqZB">
+      <node concept="2jWM_K" id="2AfSc6JxXF1" role="GyqZP">
+        <node concept="2jWLFD" id="2AfSc6JxXEX" role="2jWM_N">
+          <property role="TrG5h" value="m" />
+        </node>
+        <node concept="2jWLFD" id="2AfSc6JxXF8" role="2jWM_P">
+          <property role="TrG5h" value="q" />
+        </node>
+      </node>
+    </node>
     <node concept="GydIM" id="2AfSc6JxXFa" role="2jVTa7">
       <node concept="2jWM_K" id="2AfSc6JxXFj" role="3MT$nN">
         <node concept="2jWLFD" id="2AfSc6JxXFf" role="2jWM_N">
@@ -1125,317 +1037,411 @@
         </node>
       </node>
     </node>
-    <node concept="GyqZO" id="2AfSc6JxXET" role="GyqZB">
-      <node concept="2jWM_K" id="2AfSc6JxXF1" role="GyqZP">
-        <node concept="2jWLFD" id="2AfSc6JxXEX" role="2jWM_N">
-          <property role="TrG5h" value="m" />
-        </node>
-        <node concept="2jWLFD" id="2AfSc6JxXF8" role="2jWM_P">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
   </node>
-  <node concept="2jWMw5" id="3l440nVqpsF">
-    <property role="TrG5h" value="Test4" />
-    <property role="26WHrx" value="Given (p =&gt; q) and (q &lt;=&gt; r) proove (p =&gt; r)" />
-    <node concept="GydIM" id="3l440nVqpsY" role="2jVTa7">
-      <node concept="2jWM_K" id="3l440nVqpt7" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVqpt3" role="2jWM_N">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVqpte" role="2jWM_P">
+  <node concept="2jWMw5" id="2AfSc6Jw7pl">
+    <property role="TrG5h" value="Test2" />
+    <property role="26WHrx" value="Given (p &amp; q) prove (q | r)" />
+    <node concept="GyqZO" id="2AfSc6Jw7pn" role="GyqZB">
+      <node concept="2jWM$7" id="2AfSc6Jw7pu" role="GyqZP">
+        <node concept="2jWLFD" id="2AfSc6Jw7pr" role="2jWM__">
           <property role="TrG5h" value="q" />
         </node>
-      </node>
-    </node>
-    <node concept="GydIM" id="3l440nVqptm" role="2jVTa7">
-      <node concept="2jWMB0" id="3l440nVqptB" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVqptv" role="2jWMBa">
-          <property role="TrG5h" value="q" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVqptI" role="2jWMBd">
+        <node concept="2jWLFD" id="2AfSc6Jw7p_" role="2jWM__">
           <property role="TrG5h" value="r" />
         </node>
       </node>
     </node>
-    <node concept="2jWza5" id="3l440nVqptU" role="2jVTa7">
-      <node concept="2jWGsN" id="3l440nVqptV" role="2jWza4">
-        <node concept="2jWLFD" id="3l440nVqpu6" role="3MT$nN">
+    <node concept="GydIM" id="2AfSc6Jw7pC" role="2jVTa7">
+      <node concept="2jWMFq" id="2AfSc6Jw7pK" role="3MT$nN">
+        <node concept="2jWLFD" id="2AfSc6Jw7pH" role="2jWMFt">
           <property role="TrG5h" value="p" />
         </node>
-      </node>
-      <node concept="2jWAjR" id="3l440nVqpuc" role="2jWza4">
-        <node concept="2jWMwi" id="3l440nVqpum" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVqpsY" />
-        </node>
-        <node concept="2jWMwi" id="3l440nVqpus" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVqptV" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVqpuw" role="3MT$nN">
+        <node concept="2jWLFD" id="2AfSc6Jw7pR" role="2jWMFt">
           <property role="TrG5h" value="q" />
         </node>
       </node>
-      <node concept="2jWAjT" id="3l440nVqpuF" role="2jWza4">
-        <node concept="2jWMwi" id="3l440nVqpuT" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVqptm" />
-        </node>
-        <node concept="2jWM_K" id="3l440nVqpv0" role="3MT$nN">
-          <node concept="2jWLFD" id="3l440nVqpuW" role="2jWM_N">
-            <property role="TrG5h" value="q" />
-          </node>
-          <node concept="2jWLFD" id="3l440nVqpv7" role="2jWM_P">
-            <property role="TrG5h" value="r" />
-          </node>
-        </node>
+    </node>
+    <node concept="2jWz52" id="2AfSc6Jw7q0" role="2jVTa7">
+      <node concept="2jWMwi" id="2AfSc6Jw7qc" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jw7pC" />
       </node>
-      <node concept="2jWAjR" id="3l440nVr59R" role="2jWza4">
-        <node concept="2jWMwi" id="3l440nVr5aa" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVqpuF" />
-        </node>
-        <node concept="2jWMwi" id="3l440nVr5ag" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVqpuc" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVr5ak" role="3MT$nN">
-          <property role="TrG5h" value="r" />
-        </node>
+      <node concept="2jWLFD" id="2AfSc6Jw7qf" role="3MT$nN">
+        <property role="TrG5h" value="q" />
       </node>
     </node>
-    <node concept="2jWAjC" id="3l440nVr5bg" role="2jVTa7">
-      <node concept="2jWMwi" id="3l440nVr5bK" role="2jWFax">
-        <ref role="2jWMyc" node="3l440nVqptU" />
+    <node concept="2jWz55" id="2AfSc6JxVdj" role="2jVTa7">
+      <node concept="2jWMwi" id="2AfSc6JxVdy" role="2jWFax">
+        <ref role="2jWMyc" node="2AfSc6Jw7q0" />
       </node>
-      <node concept="2jWM_K" id="3l440nVr5bR" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVr5bN" role="2jWM_N">
-          <property role="TrG5h" value="p" />
+      <node concept="2jWM$7" id="2AfSc6JxVdC" role="3MT$nN">
+        <node concept="2jWLFD" id="2AfSc6JxVd_" role="2jWM__">
+          <property role="TrG5h" value="q" />
         </node>
-        <node concept="2jWLFD" id="3l440nVr5bY" role="2jWM_P">
-          <property role="TrG5h" value="r" />
-        </node>
-      </node>
-    </node>
-    <node concept="GyqZO" id="3l440nVqpsH" role="GyqZB">
-      <node concept="2jWM_K" id="3l440nVqpsP" role="GyqZP">
-        <node concept="2jWLFD" id="3l440nVqpsL" role="2jWM_N">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVqpsW" role="2jWM_P">
+        <node concept="2jWLFD" id="2AfSc6JxVdJ" role="2jWM__">
           <property role="TrG5h" value="r" />
         </node>
       </node>
     </node>
   </node>
-  <node concept="2jWMw5" id="3l440nVrsN1">
-    <property role="TrG5h" value="Test5" />
-    <property role="26WHrx" value="Given (p &amp; q) proove (p &lt;=&gt; q)" />
-    <node concept="GydIM" id="3l440nVrsNk" role="2jVTa7">
-      <node concept="2jWMFq" id="3l440nVrsNJ" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVrsNp" role="2jWMFt">
+  <node concept="2jWMw5" id="3JXBM6C4h$e">
+    <property role="TrG5h" value="Tautology" />
+    <property role="26WHrx" value="Proove a tautology (p | ~p)" />
+    <node concept="GyqZO" id="$u9BK_AaA7" role="GyqZB">
+      <node concept="2jWM$7" id="$u9BK_AaAe" role="GyqZP">
+        <node concept="2jWLFD" id="$u9BK_AaAb" role="2jWM__">
           <property role="TrG5h" value="p" />
         </node>
-        <node concept="2jWLFD" id="3l440nVrsNQ" role="2jWMFt">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWza5" id="3l440nVrsOD" role="2jVTa7">
-      <node concept="2jWGsN" id="3l440nVrsOE" role="2jWza4">
-        <node concept="2jWLFD" id="3l440nVrsOR" role="3MT$nN">
-          <property role="TrG5h" value="p" />
-        </node>
-      </node>
-      <node concept="2jWz52" id="3l440nVrsOf" role="2jWza4">
-        <node concept="2jWMwi" id="3l440nVrsOg" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVrsNk" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVrsOh" role="3MT$nN">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWAjC" id="3l440nVrzqG" role="2jVTa7">
-      <node concept="2jWMwi" id="3l440nVrzr1" role="2jWFax">
-        <ref role="2jWMyc" node="3l440nVrsOD" />
-      </node>
-      <node concept="2jWM_K" id="3l440nVrzr8" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVrzr4" role="2jWM_N">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVrzrf" role="2jWM_P">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWza5" id="3l440nVrzr_" role="2jVTa7">
-      <node concept="2jWGsN" id="3l440nVrzrA" role="2jWza4">
-        <node concept="2jWLFD" id="3l440nVrzrV" role="3MT$nN">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-      <node concept="2jWz52" id="3l440nVrsNY" role="2jWza4">
-        <node concept="2jWMwi" id="3l440nVrsOa" role="2jWFax">
-          <ref role="2jWMyc" node="3l440nVrsNk" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVrsOd" role="3MT$nN">
-          <property role="TrG5h" value="p" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWAjC" id="3l440nVrzuf" role="2jVTa7">
-      <node concept="2jWMwi" id="3l440nVrzuG" role="2jWFax">
-        <ref role="2jWMyc" node="3l440nVrzr_" />
-      </node>
-      <node concept="2jWM_K" id="3l440nVrzuN" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVrzuJ" role="2jWM_N">
-          <property role="TrG5h" value="q" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVrzuU" role="2jWM_P">
-          <property role="TrG5h" value="p" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWAjQ" id="3l440nVrzvo" role="2jVTa7">
-      <node concept="2jWMwi" id="3l440nVrzvU" role="2jWFax">
-        <ref role="2jWMyc" node="3l440nVrzqG" />
-      </node>
-      <node concept="2jWMwi" id="3l440nVrzw0" role="2jWFax">
-        <ref role="2jWMyc" node="3l440nVrzuf" />
-      </node>
-      <node concept="2jWMB0" id="3l440nVrzwa" role="3MT$nN">
-        <node concept="2jWLFD" id="3l440nVrzw4" role="2jWMBa">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVrzwh" role="2jWMBd">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
-    <node concept="GyqZO" id="3l440nVrsN3" role="GyqZB">
-      <node concept="2jWMB0" id="3l440nVrsNb" role="GyqZP">
-        <node concept="2jWLFD" id="3l440nVrsN7" role="2jWMBa">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFD" id="3l440nVrsNi" role="2jWMBd">
-          <property role="TrG5h" value="q" />
-        </node>
-      </node>
-    </node>
-  </node>
-  <node concept="2jWMw5" id="3l440nVt5$e">
-    <property role="TrG5h" value="Nonsense" />
-    <property role="26WHrx" value="Ex nihilo quilibet. Proove nonsense given (p &amp; ~p)." />
-    <node concept="GydIM" id="1w94$GeTp5D" role="2jVTa7">
-      <node concept="2jWMFq" id="1w94$GeTp5T" role="3MT$nN">
-        <node concept="2jWLFD" id="1w94$GeTp5Q" role="2jWMFt">
-          <property role="TrG5h" value="p" />
-        </node>
-        <node concept="2jWLFQ" id="1w94$GeTp60" role="2jWMFt">
-          <node concept="2jWLFD" id="1w94$GeTp63" role="2jWLFT">
+        <node concept="2jWLFQ" id="$u9BK_AaAl" role="2jWM__">
+          <node concept="2jWLFD" id="$u9BK_AaAo" role="2jWLFT">
             <property role="TrG5h" value="p" />
           </node>
         </node>
       </node>
     </node>
-    <node concept="2jWza5" id="1w94$GeTp6r" role="2jVTa7">
-      <node concept="2jWGsN" id="1w94$GeTp6s" role="2jWza4">
-        <node concept="2jWLFQ" id="1w94$GeTp6$" role="3MT$nN">
-          <node concept="2jWLFD" id="1w94$GeTp6A" role="2jWLFT">
-            <property role="TrG5h" value="nonsense" />
+    <node concept="2jWza5" id="$u9BK_y$0J" role="2jVTa7">
+      <node concept="2jWGsN" id="3JXBM6C4ztF" role="2jWza4">
+        <node concept="2jWLFQ" id="$u9BK_y$3a" role="3MT$nN">
+          <node concept="2jWM$7" id="3JXBM6C4ztG" role="2jWLFT">
+            <node concept="2jWLFD" id="3JXBM6C4ztH" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="5jVx7S2251s" role="2jWM__">
+              <node concept="2jWLFD" id="3JXBM6C4ztJ" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
           </node>
         </node>
       </node>
-      <node concept="2jWz52" id="1w94$GeTp71" role="2jWza4">
-        <node concept="2jWMwi" id="1w94$GeTp7c" role="2jWFax">
-          <ref role="2jWMyc" node="1w94$GeTp5D" />
-        </node>
-        <node concept="2jWLFD" id="1w94$GeTp7f" role="3MT$nN">
-          <property role="TrG5h" value="p" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWAjC" id="1w94$GeTp7G" role="2jVTa7">
-      <node concept="2jWMwi" id="1w94$GeTp80" role="2jWFax">
-        <ref role="2jWMyc" node="1w94$GeTp6r" />
-      </node>
-      <node concept="2jWM_K" id="1w94$GeTp89" role="3MT$nN">
-        <node concept="2jWLFQ" id="1w94$GeTp8j" role="2jWM_N">
-          <node concept="2jWLFD" id="1w94$GeTp85" role="2jWLFT">
-            <property role="TrG5h" value="nonsense" />
+      <node concept="2jWza5" id="3JXBM6Ca7o3" role="2jWza4">
+        <node concept="2jWGsN" id="3JXBM6Ca7o4" role="2jWza4">
+          <node concept="2jWLFD" id="3JXBM6Ca7o_" role="3MT$nN">
+            <property role="TrG5h" value="p" />
           </node>
         </node>
-        <node concept="2jWLFD" id="1w94$GeTp8g" role="2jWM_P">
-          <property role="TrG5h" value="p" />
-        </node>
-      </node>
-    </node>
-    <node concept="2jWza5" id="1w94$GeTp8J" role="2jVTa7">
-      <node concept="2jWGsN" id="1w94$GeTp8K" role="2jWza4">
-        <node concept="2jWLFQ" id="1w94$GeTp95" role="3MT$nN">
-          <node concept="2jWLFD" id="1w94$GeTp97" role="2jWLFT">
-            <property role="TrG5h" value="nonsense" />
+        <node concept="2jWz55" id="3JXBM6Ca7oF" role="2jWza4">
+          <node concept="2jWMwi" id="3JXBM6Ca7p4" role="2jWFax">
+            <ref role="2jWMyc" node="3JXBM6Ca7o4" />
+          </node>
+          <node concept="2jWM$7" id="3JXBM6Ca7oS" role="3MT$nN">
+            <node concept="2jWLFD" id="3JXBM6Ca7oP" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="3JXBM6Ca7oZ" role="2jWM__">
+              <node concept="2jWLFD" id="3JXBM6Ca7p2" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
           </node>
         </node>
       </node>
-      <node concept="2jWz52" id="1w94$GeTp9e" role="2jWza4">
-        <node concept="2jWMwi" id="1w94$GeTp9p" role="2jWFax">
-          <ref role="2jWMyc" node="1w94$GeTp5D" />
+      <node concept="2jWAjC" id="3JXBM6Ca7pK" role="2jWza4">
+        <node concept="2jWMwi" id="2AfSc6JviTh" role="2jWFax">
+          <ref role="2jWMyc" node="3JXBM6Ca7o3" />
         </node>
-        <node concept="2jWLFQ" id="1w94$GeTp9s" role="3MT$nN">
-          <node concept="2jWLFD" id="1w94$GeTp9u" role="2jWLFT">
+        <node concept="2jWM_K" id="3JXBM6Ca7qz" role="3MT$nN">
+          <node concept="2jWLFD" id="3JXBM6Ca7qv" role="2jWM_N">
+            <property role="TrG5h" value="p" />
+          </node>
+          <node concept="2jWM$7" id="3JXBM6Ca7qH" role="2jWM_P">
+            <node concept="2jWLFD" id="3JXBM6Ca7qE" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="3JXBM6Ca7qO" role="2jWM__">
+              <node concept="2jWLFD" id="3JXBM6Ca7qR" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2jWza5" id="3JXBM6Ca7rP" role="2jWza4">
+        <node concept="2jWGsN" id="3JXBM6Ca7rQ" role="2jWza4">
+          <node concept="2jWLFD" id="3JXBM6Ca7sF" role="3MT$nN">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
+        <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="5jVx7S21660" role="2jWM__">
+                <node concept="2jWLFD" id="5jVx7S21661" role="2jWLFT">
+                  <property role="TrG5h" value="p" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2jWAjC" id="$u9BK_yvcM" role="2jWza4">
+        <node concept="2jWM_K" id="$u9BK_yzWw" role="3MT$nN">
+          <node concept="2jWLFD" id="$u9BK_yzWs" role="2jWM_N">
+            <property role="TrG5h" value="p" />
+          </node>
+          <node concept="2jWLFQ" id="$u9BK_y$k$" role="2jWM_P">
+            <node concept="2jWM$7" id="$u9BK_yzWJ" role="2jWLFT">
+              <node concept="2jWLFD" id="$u9BK_yzWG" role="2jWM__">
+                <property role="TrG5h" value="p" />
+              </node>
+              <node concept="2jWLFQ" id="$u9BK_yzWQ" role="2jWM__">
+                <node concept="2jWLFD" id="$u9BK_yzWT" role="2jWLFT">
+                  <property role="TrG5h" value="p" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="2jWMwi" id="2AfSc6JviTv" role="2jWFax">
+          <ref role="2jWMyc" node="3JXBM6Ca7rP" />
+        </node>
+      </node>
+      <node concept="2jWz57" id="$u9BK_y$kO" role="2jWza4">
+        <node concept="2jWMwi" id="$u9BK_y$lO" role="2jWFax">
+          <ref role="2jWMyc" node="3JXBM6Ca7pK" />
+        </node>
+        <node concept="2jWMwi" id="$u9BK_y$lU" role="2jWFax">
+          <ref role="2jWMyc" node="$u9BK_yvcM" />
+        </node>
+        <node concept="2jWLFQ" id="$u9BK_y$lF" role="3MT$nN">
+          <node concept="2jWLFD" id="$u9BK_y$lJ" role="2jWLFT">
             <property role="TrG5h" value="p" />
           </node>
         </node>
       </node>
     </node>
-    <node concept="2jWAjC" id="1w94$GeTpab" role="2jVTa7">
-      <node concept="2jWMwi" id="1w94$GeTpaH" role="2jWFax">
-        <ref role="2jWMyc" node="1w94$GeTp8J" />
-      </node>
-      <node concept="2jWM_K" id="1w94$GeTpaO" role="3MT$nN">
-        <node concept="2jWLFQ" id="1w94$GeTpb0" role="2jWM_N">
-          <node concept="2jWLFD" id="1w94$GeTpaK" role="2jWLFT">
-            <property role="TrG5h" value="nonsense" />
+    <node concept="2jWAjC" id="$u9BK_y$oJ" role="2jVTa7">
+      <node concept="2jWM_K" id="$u9BK_y$q$" role="3MT$nN">
+        <node concept="2jWLFQ" id="$u9BK_y$v0" role="2jWM_N">
+          <node concept="2jWM$7" id="$u9BK_y$qb" role="2jWLFT">
+            <node concept="2jWLFD" id="$u9BK_y$q8" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="$u9BK_y$qi" role="2jWM__">
+              <node concept="2jWLFD" id="$u9BK_y$ql" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
           </node>
         </node>
-        <node concept="2jWLFQ" id="1w94$GeTpaV" role="2jWM_P">
-          <node concept="2jWLFD" id="1w94$GeTpaX" role="2jWLFT">
+        <node concept="2jWLFQ" id="$u9BK_y$xn" role="2jWM_P">
+          <node concept="2jWLFD" id="$u9BK_y$xp" role="2jWLFT">
             <property role="TrG5h" value="p" />
           </node>
         </node>
       </node>
+      <node concept="2jWMwi" id="2AfSc6JviTm" role="2jWFax">
+        <ref role="2jWMyc" node="$u9BK_y$0J" />
+      </node>
     </node>
-    <node concept="2jWz57" id="1w94$GeTpbB" role="2jVTa7">
-      <node concept="2jWMwi" id="1w94$GeTpcg" role="2jWFax">
-        <ref role="2jWMyc" node="1w94$GeTp7G" />
+    <node concept="2jWza5" id="$u9BK_y$yG" role="2jVTa7">
+      <node concept="2jWGsN" id="$u9BK_y$yH" role="2jWza4">
+        <node concept="2jWLFQ" id="$u9BK_y$yI" role="3MT$nN">
+          <node concept="2jWM$7" id="$u9BK_y$yJ" role="2jWLFT">
+            <node concept="2jWLFD" id="$u9BK_y$yK" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="$u9BK_y$yL" role="2jWM__">
+              <node concept="2jWLFD" id="$u9BK_y$yM" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
+          </node>
+        </node>
       </node>
-      <node concept="2jWMwi" id="1w94$GeTpcm" role="2jWFax">
-        <ref role="2jWMyc" node="1w94$GeTpab" />
+      <node concept="2jWza5" id="$u9BK_y$yN" role="2jWza4">
+        <node concept="2jWGsN" id="$u9BK_y$yO" role="2jWza4">
+          <node concept="2jWLFQ" id="$u9BK_y$_m" role="3MT$nN">
+            <node concept="2jWLFD" id="$u9BK_y$yP" role="2jWLFT">
+              <property role="TrG5h" value="p" />
+            </node>
+          </node>
+        </node>
+        <node concept="2jWz55" id="$u9BK_y$yQ" role="2jWza4">
+          <node concept="2jWMwi" id="$u9BK_y$yR" role="2jWFax">
+            <ref role="2jWMyc" node="$u9BK_y$yO" />
+          </node>
+          <node concept="2jWM$7" id="$u9BK_y$yS" role="3MT$nN">
+            <node concept="2jWLFD" id="$u9BK_y$yT" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="$u9BK_y$yU" role="2jWM__">
+              <node concept="2jWLFD" id="$u9BK_y$yV" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
+          </node>
+        </node>
       </node>
-      <node concept="2jWLFQ" id="1w94$GeTpcq" role="3MT$nN">
-        <node concept="2jWLFQ" id="1w94$GeTpcs" role="2jWLFT">
-          <node concept="2jWLFD" id="1w94$GeTpcu" role="2jWLFT">
-            <property role="TrG5h" value="nonsense" />
+      <node concept="2jWAjC" id="$u9BK_y$yW" role="2jWza4">
+        <node concept="2jWM_K" id="$u9BK_y$yZ" role="3MT$nN">
+          <node concept="2jWLFQ" id="$u9BK_y$_r" role="2jWM_N">
+            <node concept="2jWLFD" id="$u9BK_y$z0" role="2jWLFT">
+              <property role="TrG5h" value="p" />
+            </node>
+          </node>
+          <node concept="2jWM$7" id="$u9BK_y$z1" role="2jWM_P">
+            <node concept="2jWLFD" id="$u9BK_y$z2" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="$u9BK_y$z3" role="2jWM__">
+              <node concept="2jWLFD" id="$u9BK_y$z4" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="2jWMwi" id="2AfSc6JviTo" role="2jWFax">
+          <ref role="2jWMyc" node="$u9BK_y$yN" />
+        </node>
+      </node>
+      <node concept="2jWza5" id="$u9BK_y$z5" role="2jWza4">
+        <node concept="2jWGsN" id="$u9BK_y$z6" role="2jWza4">
+          <node concept="2jWLFQ" id="$u9BK_y$_w" role="3MT$nN">
+            <node concept="2jWLFD" id="$u9BK_y$z7" role="2jWLFT">
+              <property role="TrG5h" value="p" />
+            </node>
+          </node>
+        </node>
+        <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="5jVx7S22tDl" role="2jWM__">
+                <node concept="2jWLFD" id="5jVx7S22tDm" role="2jWLFT">
+                  <property role="TrG5h" value="p" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2jWAjC" id="$u9BK_y$ze" role="2jWza4">
+        <node concept="2jWM_K" id="$u9BK_y$zh" role="3MT$nN">
+          <node concept="2jWLFQ" id="$u9BK_y$__" role="2jWM_N">
+            <node concept="2jWLFD" id="$u9BK_y$zi" role="2jWLFT">
+              <property role="TrG5h" value="p" />
+            </node>
+          </node>
+          <node concept="2jWLFQ" id="$u9BK_y$zj" role="2jWM_P">
+            <node concept="2jWM$7" id="$u9BK_y$zk" role="2jWLFT">
+              <node concept="2jWLFD" id="$u9BK_y$zl" role="2jWM__">
+                <property role="TrG5h" value="p" />
+              </node>
+              <node concept="2jWLFQ" id="$u9BK_y$zm" role="2jWM__">
+                <node concept="2jWLFD" id="$u9BK_y$zn" role="2jWLFT">
+                  <property role="TrG5h" value="p" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="2jWMwi" id="2AfSc6JviTq" role="2jWFax">
+          <ref role="2jWMyc" node="$u9BK_y$z5" />
+        </node>
+      </node>
+      <node concept="2jWz57" id="$u9BK_y$zo" role="2jWza4">
+        <node concept="2jWMwi" id="$u9BK_y$zp" role="2jWFax">
+          <ref role="2jWMyc" node="$u9BK_y$yW" />
+        </node>
+        <node concept="2jWMwi" id="$u9BK_y$zq" role="2jWFax">
+          <ref role="2jWMyc" node="$u9BK_y$ze" />
+        </node>
+        <node concept="2jWLFQ" id="$u9BK_y$zr" role="3MT$nN">
+          <node concept="2jWLFQ" id="$u9BK_y$_E" role="2jWLFT">
+            <node concept="2jWLFD" id="$u9BK_y$zs" role="2jWLFT">
+              <property role="TrG5h" value="p" />
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="2jWAjD" id="$u9BK_y$A_" role="2jWza4">
+        <node concept="2jWMwi" id="$u9BK_y$B$" role="2jWFax">
+          <ref role="2jWMyc" node="$u9BK_y$zo" />
+        </node>
+        <node concept="2jWLFD" id="$u9BK_y$By" role="3MT$nN">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjC" id="$u9BK_y$yx" role="2jVTa7">
+      <node concept="2jWM_K" id="$u9BK_y$y$" role="3MT$nN">
+        <node concept="2jWLFQ" id="$u9BK_y$yB" role="2jWM_N">
+          <node concept="2jWM$7" id="$u9BK_y$yC" role="2jWLFT">
+            <node concept="2jWLFD" id="$u9BK_y$yD" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="$u9BK_y$yE" role="2jWM__">
+              <node concept="2jWLFD" id="$u9BK_y$yF" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="2jWLFD" id="$u9BK_y$yA" role="2jWM_P">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+      <node concept="2jWMwi" id="2AfSc6JviTz" role="2jWFax">
+        <ref role="2jWMyc" node="$u9BK_y$yG" />
+      </node>
+    </node>
+    <node concept="2jWz57" id="$u9BK_y$DL" role="2jVTa7">
+      <node concept="2jWMwi" id="$u9BK_y$Gw" role="2jWFax">
+        <ref role="2jWMyc" node="$u9BK_y$oJ" />
+      </node>
+      <node concept="2jWMwi" id="$u9BK_y$G_" role="2jWFax">
+        <ref role="2jWMyc" node="$u9BK_y$yx" />
+      </node>
+      <node concept="2jWLFQ" id="$u9BK_y$G8" role="3MT$nN">
+        <node concept="2jWLFQ" id="$u9BK_y$Gj" role="2jWLFT">
+          <node concept="2jWM$7" id="$u9BK_y$FV" role="2jWLFT">
+            <node concept="2jWLFD" id="$u9BK_y$FS" role="2jWM__">
+              <property role="TrG5h" value="p" />
+            </node>
+            <node concept="2jWLFQ" id="$u9BK_y$G2" role="2jWM__">
+              <node concept="2jWLFD" id="$u9BK_y$G5" role="2jWLFT">
+                <property role="TrG5h" value="p" />
+              </node>
+            </node>
           </node>
         </node>
       </node>
     </node>
-    <node concept="2jWAjD" id="1w94$GeTpd9" role="2jVTa7">
-      <node concept="2jWMwi" id="1w94$GeTpdS" role="2jWFax">
-        <ref role="2jWMyc" node="1w94$GeTpbB" />
+    <node concept="2jWAjD" id="$u9BK_y$IN" role="2jVTa7">
+      <node concept="2jWMwi" id="$u9BK_y$Li" role="2jWFax">
+        <ref role="2jWMyc" node="$u9BK_y$DL" />
       </node>
-      <node concept="2jWLFD" id="1w94$GeTpdV" role="3MT$nN">
-        <property role="TrG5h" value="nonsense" />
-      </node>
-    </node>
-    <node concept="GyqZO" id="3l440nVt5$g" role="GyqZB">
-      <node concept="2jWLFD" id="3l440nVt5$k" role="GyqZP">
-        <property role="TrG5h" value="nonsense" />
+      <node concept="2jWM$7" id="$u9BK_y$L6" role="3MT$nN">
+        <node concept="2jWLFD" id="$u9BK_y$L3" role="2jWM__">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFQ" id="$u9BK_y$Ld" role="2jWM__">
+          <node concept="2jWLFD" id="$u9BK_y$Lg" role="2jWLFT">
+            <property role="TrG5h" value="p" />
+          </node>
+        </node>
       </node>
     </node>
   </node>
   <node concept="2jWMw5" id="5A8qZLXfUvB">
     <property role="TrG5h" value="Sample" />
     <property role="26WHrx" value="Proove (cloudy) given (rain =&gt; cloudy) and (rain)" />
+    <node concept="GyqZO" id="5A8qZLXfUvD" role="GyqZB">
+      <node concept="2jWLFD" id="5A8qZLXfUvH" role="GyqZP">
+        <property role="TrG5h" value="cloudy" />
+      </node>
+    </node>
     <node concept="GydIM" id="5A8qZLXfUvX" role="2jVTa7">
       <node concept="2jWM_K" id="5A8qZLXfUw8" role="3MT$nN">
         <node concept="2jWLFD" id="5A8qZLXfUw4" role="2jWM_N">
@@ -1462,15 +1468,17 @@
         <property role="TrG5h" value="cloudy" />
       </node>
     </node>
-    <node concept="GyqZO" id="5A8qZLXfUvD" role="GyqZB">
-      <node concept="2jWLFD" id="5A8qZLXfUvH" role="GyqZP">
-        <property role="TrG5h" value="cloudy" />
-      </node>
-    </node>
   </node>
   <node concept="2jWMw5" id="5A8qZLXfUwO">
     <property role="TrG5h" value="Test6" />
     <property role="26WHrx" value="Given ((p =&gt; q) &amp; ~q) proove ~p" />
+    <node concept="GyqZO" id="5A8qZLXfUwQ" role="GyqZB">
+      <node concept="2jWLFQ" id="5A8qZLXfUwX" role="GyqZP">
+        <node concept="2jWLFD" id="5A8qZLXfUwU" role="2jWLFT">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+    </node>
     <node concept="GydIM" id="5A8qZLXfUx1" role="2jVTa7">
       <node concept="2jWMFq" id="5A8qZLXfUxk" role="3MT$nN">
         <node concept="2jWM_K" id="5A8qZLXfUxa" role="2jWMFt">
@@ -1577,13 +1585,6 @@
         </node>
       </node>
     </node>
-    <node concept="GyqZO" id="5A8qZLXfUwQ" role="GyqZB">
-      <node concept="2jWLFQ" id="5A8qZLXfUwX" role="GyqZP">
-        <node concept="2jWLFD" id="5A8qZLXfUwU" role="2jWLFT">
-          <property role="TrG5h" value="p" />
-        </node>
-      </node>
-    </node>
   </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/behavior.mps b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/behavior.mps
index 5c6b4467..369940a9 100644
--- a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/behavior.mps
+++ b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/behavior.mps
@@ -5,7 +5,106 @@
     <use id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior" version="1" />
     <devkit ref="2677cb18-f558-4e33-bc38-a5139cee06dc(jetbrains.mps.devkit.language-design)" />
   </languages>
-  <imports />
-  <registry />
+  <imports>
+    <import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" />
+    <import index="27wh" ref="r:459ba7ac-2a61-40fc-bcc4-f13a7956cbeb(jetbrains.mps.logic.propositional.structure)" implicit="true" />
+  </imports>
+  <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" />
+        <reference id="1225194472831" name="overriddenMethod" index="13i0hy" />
+      </concept>
+    </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="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
+        <child id="1137022507850" name="body" index="2VODD2" />
+      </concept>
+      <concept id="1070534644030" name="jetbrains.mps.baseLanguage.structure.BooleanType" flags="in" index="10P_77" />
+      <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>
+      <concept id="1068580123132" name="jetbrains.mps.baseLanguage.structure.BaseMethodDeclaration" flags="ng" index="3clF44">
+        <child id="1068580123133" name="returnType" index="3clF45" />
+        <child id="1068580123134" name="parameter" index="3clF46" />
+        <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="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
+        <child id="1068581517665" name="statement" index="3cqZAp" />
+      </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="1180031783296" name="jetbrains.mps.lang.smodel.structure.Concept_IsSubConceptOfOperation" flags="nn" index="2Zo12i">
+        <child id="1180031783297" name="conceptArgument" index="2Zo12j" />
+      </concept>
+      <concept id="6677504323281689838" name="jetbrains.mps.lang.smodel.structure.SConceptType" flags="in" index="3bZ5Sz" />
+    </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>
+  </registry>
+  <node concept="13h7C7" id="3w0n0hzjKQg">
+    <property role="3GE5qa" value="proof" />
+    <ref role="13h7C2" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
+    <node concept="13hLZK" id="3w0n0hzjKQh" role="13h7CW">
+      <node concept="3clFbS" id="3w0n0hzjKQi" role="2VODD2" />
+    </node>
+    <node concept="13i0hz" id="3w0n0hzjKQr" role="13h7CS">
+      <property role="13i0iv" value="false" />
+      <property role="13i0it" value="false" />
+      <property role="TrG5h" value="isRuleSupported" />
+      <ref role="13i0hy" to="qd7f:3w0n0hzjKLG" resolve="isRuleSupported" />
+      <node concept="3Tm1VV" id="3w0n0hzjKQu" role="1B3o_S" />
+      <node concept="3clFbS" id="3w0n0hzjKQx" role="3clF47">
+        <node concept="3clFbF" id="3w0n0hzjKUz" role="3cqZAp">
+          <node concept="2OqwBi" id="3w0n0hzjL4O" role="3clFbG">
+            <node concept="37vLTw" id="3w0n0hzjKUy" role="2Oq$k0">
+              <ref role="3cqZAo" node="3w0n0hzjKQy" resolve="ruleConcept" />
+            </node>
+            <node concept="2Zo12i" id="3w0n0hzjLsE" role="2OqNvi">
+              <node concept="chp4Y" id="3w0n0hzjLys" role="2Zo12j">
+                <ref role="cht4Q" to="27wh:3w0n0hziLcf" resolve="PropositionalRule" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="37vLTG" id="3w0n0hzjKQy" role="3clF46">
+        <property role="TrG5h" value="ruleConcept" />
+        <node concept="3bZ5Sz" id="3w0n0hzjKQz" role="1tU5fm" />
+      </node>
+      <node concept="10P_77" id="3w0n0hzjKQ$" role="3clF45" />
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/constraints.mps b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/constraints.mps
index 4400b921..fedc5daa 100644
--- a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/constraints.mps
+++ b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/constraints.mps
@@ -5,18 +5,30 @@
     <use id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints" version="4" />
     <use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="5" />
     <use id="daafa647-f1f7-4b0b-b096-69cd7c8408c0" name="jetbrains.mps.baseLanguage.regexp" version="0" />
+    <use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="8" />
+    <use id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections" version="0" />
+    <use id="fd392034-7849-419d-9071-12563d152375" name="jetbrains.mps.baseLanguage.closures" version="0" />
     <devkit ref="00000000-0000-4000-0000-5604ebd4f22c(jetbrains.mps.devkit.aspect.constraints)" />
   </languages>
   <imports>
     <import index="27wh" ref="r:459ba7ac-2a61-40fc-bcc4-f13a7956cbeb(jetbrains.mps.logic.propositional.structure)" />
     <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
     <import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" />
+    <import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
+    <import index="qd7f" ref="r:6e0181fc-40ea-4aea-a8b0-3ba2d104ddef(jetbrains.mps.fitch.behavior)" implicit="true" />
   </imports>
   <registry>
     <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="1137021947720" name="jetbrains.mps.baseLanguage.structure.ConceptFunction" flags="in" index="2VMwT0">
         <child id="1137022507850" name="body" index="2VODD2" />
       </concept>
+      <concept id="1068580123155" name="jetbrains.mps.baseLanguage.structure.ExpressionStatement" flags="nn" index="3clFbF">
+        <child id="1068580123156" name="expression" index="3clFbG" />
+      </concept>
       <concept id="1068580123136" name="jetbrains.mps.baseLanguage.structure.StatementList" flags="sn" stub="5293379017992965193" index="3clFbS">
         <child id="1068581517665" name="statement" index="3cqZAp" />
       </concept>
@@ -26,8 +38,15 @@
       <concept id="1068581242878" name="jetbrains.mps.baseLanguage.structure.ReturnStatement" flags="nn" index="3cpWs6">
         <child id="1068581517676" name="expression" index="3cqZAk" />
       </concept>
+      <concept id="1204053956946" name="jetbrains.mps.baseLanguage.structure.IMethodCall" flags="ng" index="1ndlxa">
+        <reference id="1068499141037" name="baseMethodDeclaration" index="37wK5l" />
+        <child id="1068499141038" name="actualArgument" index="37wK5m" />
+      </concept>
     </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="4303308395523096213" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_childConcept" flags="ng" index="2DD5aU" />
       <concept id="1147467115080" name="jetbrains.mps.lang.constraints.structure.NodePropertyConstraint" flags="ng" index="EnEH3">
         <reference id="1147467295099" name="applicableProperty" index="EomxK" />
         <child id="1212097481299" name="propertyValidator" index="QCWH9" />
@@ -35,10 +54,25 @@
       <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" />
     </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="1171407110247" name="jetbrains.mps.lang.smodel.structure.Node_GetAncestorOperation" flags="nn" index="2Xjw5R" />
+      <concept id="1144100932627" name="jetbrains.mps.lang.smodel.structure.OperationParm_Inclusion" flags="ng" index="1xIGOp" />
+      <concept id="1144101972840" name="jetbrains.mps.lang.smodel.structure.OperationParm_Concept" flags="ng" index="1xMEDy">
+        <child id="1207343664468" name="conceptArgument" index="ri$Ld" />
+      </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" />
@@ -97,5 +131,32 @@
       </node>
     </node>
   </node>
+  <node concept="1M2fIO" id="3w0n0hzjH5f">
+    <property role="3GE5qa" value="proof.rule" />
+    <ref role="1M2myG" to="27wh:3w0n0hziLcf" resolve="PropositionalRule" />
+    <node concept="9S07l" id="3w0n0hzjH5g" role="9Vyp8">
+      <node concept="3clFbS" id="3w0n0hzjH5h" role="2VODD2">
+        <node concept="3clFbF" id="3w0n0hzjEJQ" role="3cqZAp">
+          <node concept="2OqwBi" id="3w0n0hzjFH7" role="3clFbG">
+            <node concept="2OqwBi" id="3w0n0hzjEZ0" role="2Oq$k0">
+              <node concept="nLn13" id="3w0n0hzjEJP" role="2Oq$k0" />
+              <node concept="2Xjw5R" id="3w0n0hzjFfL" role="2OqNvi">
+                <node concept="1xMEDy" id="3w0n0hzjSnx" role="1xVPHs">
+                  <node concept="chp4Y" id="3w0n0hzjS$2" role="ri$Ld">
+                    <ref role="cht4Q" to="jfgh:3JXBM6C5urr" resolve="Root" />
+                  </node>
+                </node>
+                <node concept="1xIGOp" id="3w0n0hzjSWs" role="1xVPHs" />
+              </node>
+            </node>
+            <node concept="2qgKlT" id="3w0n0hzjTgg" role="2OqNvi">
+              <ref role="37wK5l" to="qd7f:3w0n0hzjKLG" resolve="isRuleSupported" />
+              <node concept="2DD5aU" id="3w0n0hzjTDM" role="37wK5m" />
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/editor.mps b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/editor.mps
index db357180..4e10c2d2 100644
--- a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/editor.mps
+++ b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/editor.mps
@@ -14,6 +14,8 @@
     <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
     <import index="tpfp" ref="r:00000000-0000-4000-0000-011c89590519(jetbrains.mps.baseLanguage.regexp.jetbrains.mps.regexp.accessory)" />
     <import index="jfgh" ref="r:2003997c-f9a6-418f-99d4-03e1285a3e13(jetbrains.mps.fitch.structure)" />
+    <import index="8v9h" ref="r:873e37f0-b045-47b9-ae9e-db79c2628975(jetbrains.mps.fitch.editor)" />
+    <import index="tpco" ref="r:00000000-0000-4000-0000-011c89590284(jetbrains.mps.lang.core.editor)" implicit="true" />
   </imports>
   <registry>
     <language id="18bc6592-03a6-4e29-a83a-7ff23bde13ba" name="jetbrains.mps.lang.editor">
@@ -23,6 +25,9 @@
       </concept>
       <concept id="1071666914219" name="jetbrains.mps.lang.editor.structure.ConceptEditorDeclaration" flags="ig" index="24kQdi" />
       <concept id="1597643335227097138" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_TransformationMenu_node" flags="ng" index="7Obwk" />
+      <concept id="6822301196700715228" name="jetbrains.mps.lang.editor.structure.ConceptEditorHintDeclarationReference" flags="ig" index="2aJ2om">
+        <reference id="5944657839026714445" name="hint" index="2$4xQ3" />
+      </concept>
       <concept id="1140524381322" name="jetbrains.mps.lang.editor.structure.CellModel_ListWithRole" flags="ng" index="2czfm3">
         <property id="1140524450557" name="separatorText" index="2czwfO" />
         <child id="1140524464360" name="cellLayout" index="2czzBx" />
@@ -32,8 +37,11 @@
       <concept id="1196434649611" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_SimpleString" flags="ng" index="2h3Zct">
         <property id="1196434851095" name="text" index="2h4Kg1" />
       </concept>
+      <concept id="1106270549637" name="jetbrains.mps.lang.editor.structure.CellLayout_Horizontal" flags="nn" index="2iRfu4" />
+      <concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
       <concept id="3459162043708467089" name="jetbrains.mps.lang.editor.structure.CellActionMap_CanExecuteFunction" flags="in" index="jK8Ss" />
       <concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
+      <concept id="1237308012275" name="jetbrains.mps.lang.editor.structure.IndentLayoutNewLineStyleClassItem" flags="ln" index="ljvvj" />
       <concept id="1233148810477" name="jetbrains.mps.lang.editor.structure.InlineStyleDeclaration" flags="ng" index="tppnM" />
       <concept id="1177327274449" name="jetbrains.mps.lang.editor.structure.QueryFunctionParameter_pattern" flags="nn" index="ub8z3" />
       <concept id="1177327570013" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_Substitute" flags="in" index="ucgPf" />
@@ -41,6 +49,9 @@
         <child id="8478191136883534238" name="features" index="upBLP" />
       </concept>
       <concept id="1177335944525" name="jetbrains.mps.lang.editor.structure.QueryFunction_SubstituteMenu_SubstituteString" flags="in" index="uGdhv" />
+      <concept id="4242538589859161874" name="jetbrains.mps.lang.editor.structure.ExplicitHintsSpecification" flags="ng" index="2w$q5c">
+        <child id="4242538589859162459" name="hints" index="2w$qW5" />
+      </concept>
       <concept id="1080736578640" name="jetbrains.mps.lang.editor.structure.BaseEditorComponent" flags="ig" index="2wURMF">
         <child id="1080736633877" name="cellModel" index="2wV5jI" />
       </concept>
@@ -56,6 +67,9 @@
         <child id="1638911550608610281" name="executeFunction" index="IWgqQ" />
         <child id="5692353713941573325" name="textFunction" index="1hCUd6" />
       </concept>
+      <concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
+        <reference id="1078939183255" name="editorComponent" index="PMmxG" />
+      </concept>
       <concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
         <property id="1186414551515" name="flag" index="VOm3f" />
       </concept>
@@ -90,6 +104,7 @@
       <concept id="5692353713941573329" name="jetbrains.mps.lang.editor.structure.QueryFunction_TransformationMenu_ActionLabelText" flags="ig" index="1hCUdq" />
       <concept id="3308396621974580100" name="jetbrains.mps.lang.editor.structure.SubstituteMenu_Default" flags="ng" index="3p36aQ" />
       <concept id="1139848536355" name="jetbrains.mps.lang.editor.structure.CellModel_WithRole" flags="ng" index="1$h60E">
+        <property id="1139852716018" name="noTargetText" index="1$x2rV" />
         <reference id="1140103550593" name="relationDeclaration" index="1NtTu8" />
       </concept>
       <concept id="1073389214265" name="jetbrains.mps.lang.editor.structure.EditorCellModel" flags="ng" index="3EYTF0">
@@ -108,7 +123,9 @@
         <child id="1219418656006" name="styleItem" index="3F10Kt" />
       </concept>
       <concept id="1073389882823" name="jetbrains.mps.lang.editor.structure.CellModel_RefNode" flags="sg" stub="730538219795960754" index="3F1sOY" />
-      <concept id="1073390211982" name="jetbrains.mps.lang.editor.structure.CellModel_RefNodeList" flags="sg" stub="2794558372793454595" index="3F2HdR" />
+      <concept id="1073390211982" name="jetbrains.mps.lang.editor.structure.CellModel_RefNodeList" flags="sg" stub="2794558372793454595" index="3F2HdR">
+        <child id="7279578193766667846" name="addHints" index="78xua" />
+      </concept>
       <concept id="5624877018228267058" name="jetbrains.mps.lang.editor.structure.ITransformationMenu" flags="ng" index="3INCJE">
         <child id="1638911550608572412" name="sections" index="IW6Ez" />
       </concept>
@@ -1231,5 +1248,154 @@
       </node>
     </node>
   </node>
+  <node concept="24kQdi" id="3JXBM6C3URg">
+    <property role="3GE5qa" value="proof" />
+    <ref role="1XX52x" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
+    <node concept="3EZMnI" id="3JXBM6C3URi" role="2wV5jI">
+      <node concept="PMmxH" id="3w0n0hzhNuL" role="3EZMnx">
+        <ref role="PMmxG" to="tpco:2wZex4PafBj" resolve="alias" />
+      </node>
+      <node concept="3F0A7n" id="3JXBM6C4h$I" role="3EZMnx">
+        <ref role="1NtTu8" to="tpck:h0TrG11" resolve="name" />
+        <node concept="ljvvj" id="3JXBM6C4h$R" role="3F10Kt">
+          <property role="VOm3f" value="true" />
+        </node>
+      </node>
+      <node concept="3F0ifn" id="2AfSc6Jvjpp" role="3EZMnx">
+        <property role="3F0ifm" value="" />
+        <node concept="ljvvj" id="2AfSc6Jvjpq" role="3F10Kt">
+          <property role="VOm3f" value="true" />
+        </node>
+      </node>
+      <node concept="3F0A7n" id="2AfSc6Jvjoy" role="3EZMnx">
+        <ref role="1NtTu8" to="jfgh:2AfSc6Jvjow" resolve="description" />
+        <node concept="ljvvj" id="2AfSc6Jvjs0" role="3F10Kt">
+          <property role="VOm3f" value="true" />
+        </node>
+      </node>
+      <node concept="3F0ifn" id="$u9BK__SIy" role="3EZMnx">
+        <property role="3F0ifm" value="" />
+        <node concept="ljvvj" id="$u9BK__SJr" role="3F10Kt">
+          <property role="VOm3f" value="true" />
+        </node>
+      </node>
+      <node concept="3EZMnI" id="$u9BK__SDZ" role="3EZMnx">
+        <node concept="ljvvj" id="$u9BK__SHA" role="3F10Kt">
+          <property role="VOm3f" value="true" />
+        </node>
+        <node concept="VPM3Z" id="$u9BK__SE1" role="3F10Kt">
+          <property role="VOm3f" value="false" />
+        </node>
+        <node concept="3F0ifn" id="$u9BK__SFC" role="3EZMnx">
+          <property role="3F0ifm" value="Goal:" />
+        </node>
+        <node concept="l2Vlx" id="$u9BK__SE4" role="2iSdaV" />
+        <node concept="3F1sOY" id="$u9BK__SCz" role="3EZMnx">
+          <property role="1$x2rV" value="&lt;no goal&gt;" />
+          <ref role="1NtTu8" to="jfgh:$u9BK__SAr" resolve="goal" />
+        </node>
+      </node>
+      <node concept="3EZMnI" id="$u9BK__SGu" role="3EZMnx">
+        <node concept="VPM3Z" id="$u9BK__SGw" role="3F10Kt">
+          <property role="VOm3f" value="false" />
+        </node>
+        <node concept="ljvvj" id="$u9BK__SHv" role="3F10Kt">
+          <property role="VOm3f" value="true" />
+        </node>
+        <node concept="3F0ifn" id="$u9BK__SHp" role="3EZMnx">
+          <property role="3F0ifm" value="Proof:" />
+        </node>
+        <node concept="l2Vlx" id="$u9BK__SGz" role="2iSdaV" />
+      </node>
+      <node concept="3EZMnI" id="$u9BK_yCN6" role="3EZMnx">
+        <node concept="3EZMnI" id="$u9BK_z1QP" role="3EZMnx">
+          <node concept="VPM3Z" id="$u9BK_z1QR" role="3F10Kt">
+            <property role="VOm3f" value="false" />
+          </node>
+          <node concept="2iRkQZ" id="$u9BK_z1QU" role="2iSdaV" />
+          <node concept="3EZMnI" id="$u9BK_z6et" role="3EZMnx">
+            <node concept="l2Vlx" id="$u9BK_z6eu" role="2iSdaV" />
+            <node concept="VPM3Z" id="$u9BK_z6ev" role="3F10Kt">
+              <property role="VOm3f" value="false" />
+            </node>
+            <node concept="3F2HdR" id="$u9BK_z6ez" role="3EZMnx">
+              <property role="2czwfO" value=" " />
+              <ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
+              <node concept="l2Vlx" id="$u9BK_z6e$" role="2czzBx" />
+              <node concept="tppnM" id="$u9BK_zt0T" role="sWeuL">
+                <node concept="ljvvj" id="$u9BK_zt0V" role="3F10Kt">
+                  <property role="VOm3f" value="true" />
+                </node>
+              </node>
+              <node concept="2w$q5c" id="5RfK0kxj3Yz" role="78xua">
+                <node concept="2aJ2om" id="5RfK0kxj3Y$" role="2w$qW5">
+                  <ref role="2$4xQ3" to="8v9h:$u9BK_z27v" resolve="ID" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="3EZMnI" id="$u9BK_yCN7" role="3EZMnx">
+          <node concept="VPM3Z" id="$u9BK_yCN8" role="3F10Kt">
+            <property role="VOm3f" value="false" />
+          </node>
+          <node concept="2iRkQZ" id="$u9BK_yCNa" role="2iSdaV" />
+          <node concept="3EZMnI" id="3JXBM6C6j0E" role="3EZMnx">
+            <node concept="VPM3Z" id="3JXBM6C6j0G" role="3F10Kt">
+              <property role="VOm3f" value="false" />
+            </node>
+            <node concept="l2Vlx" id="3JXBM6C6j0J" role="2iSdaV" />
+            <node concept="3F2HdR" id="3JXBM6C3URp" role="3EZMnx">
+              <property role="2czwfO" value=" " />
+              <ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
+              <node concept="l2Vlx" id="3JXBM6C3URr" role="2czzBx" />
+              <node concept="tppnM" id="3JXBM6C3URw" role="sWeuL">
+                <node concept="ljvvj" id="3JXBM6C3URy" role="3F10Kt">
+                  <property role="VOm3f" value="true" />
+                </node>
+              </node>
+              <node concept="3F0ifn" id="3JXBM6C3UR$" role="2czzBI">
+                <property role="3F0ifm" value="" />
+                <property role="ilYzB" value="&lt;no steps&gt;" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="2iRfu4" id="$u9BK_yCNb" role="2iSdaV" />
+        <node concept="3EZMnI" id="$u9BK_zG5o" role="3EZMnx">
+          <node concept="3EZMnI" id="$u9BK_$Qxk" role="3EZMnx">
+            <node concept="l2Vlx" id="$u9BK_$Qxl" role="2iSdaV" />
+            <node concept="VPM3Z" id="$u9BK_$Qxm" role="3F10Kt">
+              <property role="VOm3f" value="false" />
+            </node>
+            <node concept="3F2HdR" id="$u9BK_$Qxn" role="3EZMnx">
+              <property role="2czwfO" value=" " />
+              <ref role="1NtTu8" to="jfgh:3JXBM6C4wQA" resolve="content" />
+              <node concept="l2Vlx" id="$u9BK_$Qxo" role="2czzBx" />
+              <node concept="tppnM" id="$u9BK_$Qxp" role="sWeuL">
+                <node concept="ljvvj" id="$u9BK_$Qxq" role="3F10Kt">
+                  <property role="VOm3f" value="true" />
+                </node>
+              </node>
+              <node concept="2w$q5c" id="$u9BK_$QxA" role="78xua">
+                <node concept="2aJ2om" id="$u9BK_$QxB" role="2w$qW5">
+                  <ref role="2$4xQ3" to="8v9h:$u9BK_zG6f" resolve="BASIS" />
+                </node>
+              </node>
+            </node>
+          </node>
+          <node concept="VPM3Z" id="$u9BK_zG5q" role="3F10Kt">
+            <property role="VOm3f" value="false" />
+          </node>
+          <node concept="2iRkQZ" id="$u9BK_zG5t" role="2iSdaV" />
+        </node>
+      </node>
+      <node concept="l2Vlx" id="3JXBM6C3URl" role="2iSdaV" />
+    </node>
+  </node>
+  <node concept="3p36aQ" id="3JXBM6C6F7z">
+    <property role="3GE5qa" value="proof" />
+    <ref role="aqKnT" to="27wh:3JXBM6C3Fs$" resolve="PropositionalProof" />
+  </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/structure.mps b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/structure.mps
index 3626d0ca..cad0e6a4 100644
--- a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/structure.mps
+++ b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/structure.mps
@@ -24,6 +24,7 @@
         <reference id="1169127628841" name="intfc" index="PrY4T" />
       </concept>
       <concept id="1071489090640" name="jetbrains.mps.lang.structure.structure.ConceptDeclaration" flags="ig" index="1TIwiD">
+        <property id="1096454100552" name="rootable" index="19KtqR" />
         <reference id="1071489389519" name="extends" index="1TJDcQ" />
         <child id="1169129564478" name="implements" index="PzmwI" />
       </concept>
@@ -170,6 +171,9 @@
     <property role="34LRSv" value="&amp;E" />
     <property role="R4oN_" value="And Elimination" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcg" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3URE">
     <property role="EcuMT" value="4322786184247881194" />
@@ -178,6 +182,9 @@
     <property role="34LRSv" value="&amp;I" />
     <property role="R4oN_" value="And Introduction" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLci" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3ZJm">
     <property role="EcuMT" value="4322786184247901142" />
@@ -186,6 +193,9 @@
     <property role="34LRSv" value="=&gt;E" />
     <property role="R4oN_" value="Implication Elimination" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLck" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3ZJ9">
     <property role="EcuMT" value="4322786184247901129" />
@@ -194,6 +204,9 @@
     <property role="34LRSv" value="=&gt;I" />
     <property role="R4oN_" value="Implication Introduction" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcm" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3ZJo">
     <property role="EcuMT" value="4322786184247901144" />
@@ -202,6 +215,9 @@
     <property role="34LRSv" value="&lt;=&gt;E" />
     <property role="R4oN_" value="Biconditional Elimination" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLco" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3ZJn">
     <property role="EcuMT" value="4322786184247901143" />
@@ -210,6 +226,9 @@
     <property role="34LRSv" value="&lt;=&gt;I" />
     <property role="R4oN_" value="Biconditional Introduction" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcq" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3ZJ8">
     <property role="EcuMT" value="4322786184247901128" />
@@ -218,6 +237,9 @@
     <property role="34LRSv" value="~E" />
     <property role="R4oN_" value="Negation Elimination" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcs" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3UTA">
     <property role="EcuMT" value="4322786184247881318" />
@@ -226,6 +248,9 @@
     <property role="34LRSv" value="~I" />
     <property role="R4oN_" value="Negation Introduction" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcu" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3UT_">
     <property role="EcuMT" value="4322786184247881317" />
@@ -234,6 +259,9 @@
     <property role="34LRSv" value="|E" />
     <property role="R4oN_" value="Or Elimination" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcw" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
   </node>
   <node concept="1TIwiD" id="3JXBM6C3UT$">
     <property role="EcuMT" value="4322786184247881316" />
@@ -242,6 +270,28 @@
     <property role="34LRSv" value="|I" />
     <property role="R4oN_" value="OrIntroduction" />
     <ref role="1TJDcQ" to="jfgh:3JXBM6C3FsA" resolve="Judgement" />
+    <node concept="PrWs8" id="3w0n0hziLcy" role="PzmwI">
+      <ref role="PrY4T" node="3w0n0hziLcf" resolve="PropositionalRule" />
+    </node>
+  </node>
+  <node concept="1TIwiD" id="3JXBM6C3Fs$">
+    <property role="EcuMT" value="4322786184247818020" />
+    <property role="TrG5h" value="PropositionalProof" />
+    <property role="19KtqR" value="true" />
+    <property role="34LRSv" value="Propositional Proof" />
+    <property role="3GE5qa" value="proof" />
+    <ref role="1TJDcQ" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
+    <node concept="PrWs8" id="3JXBM6C3URC" role="PzmwI">
+      <ref role="PrY4T" to="tpck:h0TrEE$" resolve="INamedConcept" />
+    </node>
+    <node concept="PrWs8" id="3JXBM6C5v8v" role="PzmwI">
+      <ref role="PrY4T" to="jfgh:3JXBM6C5urr" resolve="Root" />
+    </node>
+  </node>
+  <node concept="PlHQZ" id="3w0n0hziLcf">
+    <property role="EcuMT" value="4035326440039453455" />
+    <property role="3GE5qa" value="proof.rule" />
+    <property role="TrG5h" value="PropositionalRule" />
   </node>
 </model>
 
diff --git a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/types.mps b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/types.mps
index 63077515..67a8660d 100644
--- a/samples/fitch/languages/jetbrains.mps.logic.propositional/models/types.mps
+++ b/samples/fitch/languages/jetbrains.mps.logic.propositional/models/types.mps
@@ -5356,8 +5356,8 @@
                     <node concept="2OqwBi" id="2YqrT$P7QYz" role="2Oq$k0">
                       <node concept="1PxgMI" id="2YqrT$P7QY$" role="2Oq$k0">
                         <property role="1BlNFB" value="true" />
-                        <node concept="chp4Y" id="2YqrT$P7QY_" role="3oSUPX">
-                          <ref role="cht4Q" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
+                        <node concept="chp4Y" id="3w0n0hzgXvI" role="3oSUPX">
+                          <ref role="cht4Q" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
                         </node>
                         <node concept="2OqwBi" id="2YqrT$P7QYA" role="1m5AlR">
                           <node concept="3A2sRY" id="2YqrT$P7QYB" role="2Oq$k0">
@@ -5415,8 +5415,8 @@
                   <node concept="2OqwBi" id="2YqrT$P7QS9" role="2Oq$k0">
                     <node concept="1PxgMI" id="2YqrT$P7QSa" role="2Oq$k0">
                       <property role="1BlNFB" value="true" />
-                      <node concept="chp4Y" id="2YqrT$P7QSb" role="3oSUPX">
-                        <ref role="cht4Q" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
+                      <node concept="chp4Y" id="3w0n0hzgXrv" role="3oSUPX">
+                        <ref role="cht4Q" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
                       </node>
                       <node concept="2OqwBi" id="2YqrT$P7QSc" role="1m5AlR">
                         <node concept="3A2sRY" id="2YqrT$P7QSd" role="2Oq$k0">
@@ -5450,8 +5450,8 @@
                 <node concept="2OqwBi" id="2YqrT$P7JQA" role="2Oq$k0">
                   <node concept="1PxgMI" id="2YqrT$P7J$X" role="2Oq$k0">
                     <property role="1BlNFB" value="true" />
-                    <node concept="chp4Y" id="2YqrT$P7JEG" role="3oSUPX">
-                      <ref role="cht4Q" to="jfgh:3JXBM6C3Fs$" resolve="Proof" />
+                    <node concept="chp4Y" id="3w0n0hzgWPN" role="3oSUPX">
+                      <ref role="cht4Q" to="jfgh:3w0n0hzgWvH" resolve="AbstractProof" />
                     </node>
                     <node concept="2OqwBi" id="2YqrT$P7IdR" role="1m5AlR">
                       <node concept="3A2sRY" id="2YqrT$P7I5i" role="2Oq$k0">