diff --git a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
index 10f3d1bdda07dff6b64b40d9ba93382464ae0089..f53dc66b535739997543cd9c34fdcadf6142faa5 100644
--- a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
+++ b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
@@ -10,9 +10,11 @@ import info.kwarc.mmt.lf.{Apply, Arrow, OfType, Pi}
 import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
 import info.kwarc.mmt.api.utils.URI
 
+import scala.collection.mutable
+
 object StepUntil {
   val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
-  val path: GlobalName = ns ? "StepUntilWrap" ? "stepUntil"
+  val path: GlobalName = ns ? "StepUntilRaw" ? "stepUntil"
   val term: OMID = OMS(path)
   def apply(iv: Term, f: Term, tC: Term): Term = OMA(this.term, List(iv, f, tC))
   def unapply(tm : Term) : Option[(Term,Term,Term)] = tm match {
@@ -35,21 +37,21 @@ object StepUntilRule extends ParametricRule {
   case class StepUntilComp(truetm: Term) extends ComputationRule(StepUntil.path) {
     override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
       case StepUntil(iv, f, tC) =>
-        var values = Seq[Term]()
+        val values = mutable.ListBuffer[Term]()
         var iter = 0
         var cur = iv
         while (iter < DEBUG_MAX_ITER_COUNT) {
           iter += 1
           check.tryToCheckWithoutDelay(Equality(stack, Apply(tC, cur), truetm, None)) match {
             case Some(true) =>
-              return Simplify(Ls(values : _*))
+              return Simplify(Ls(values.toSeq : _*))
             case Some(false) | None =>
-              values = values :+ cur
-              cur = Apply(f, cur)
+              values += cur
+              cur = check.simplify(Apply(f, cur))
           }
         }
         // todo: try to log something via stack, history, check, or this
-        Simplify(Ls(values : _*))
+        Simplify(Ls(values.toSeq : _*))
       case _ => Simplifiability.NoRecurse
     }
   }
diff --git a/source/.idea/.gitignore b/source/.idea/.gitignore
deleted file mode 100644
index 26d33521af10bcc7fd8cea344038eaaeb78d0ef5..0000000000000000000000000000000000000000
--- a/source/.idea/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-# Default ignored files
-/shelf/
-/workspace.xml
diff --git a/source/.idea/codeStyles/Project.xml b/source/.idea/codeStyles/Project.xml
deleted file mode 100644
index 508ba9cf2f25e1410213f6515fb6a36551ff7591..0000000000000000000000000000000000000000
--- a/source/.idea/codeStyles/Project.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
-  <code_scheme name="Project" version="173">
-    <option name="OTHER_INDENT_OPTIONS">
-      <value>
-        <option name="TAB_SIZE" value="2" />
-      </value>
-    </option>
-    <option name="LINE_SEPARATOR" value="&#10;" />
-    <option name="FORMATTER_TAGS_ENABLED" value="true" />
-    <ScalaCodeStyleSettings>
-      <option name="MULTILINE_STRING_CLOSING_QUOTES_ON_NEW_LINE" value="true" />
-    </ScalaCodeStyleSettings>
-  </code_scheme>
-</component>
\ No newline at end of file
diff --git a/source/.idea/codeStyles/codeStyleConfig.xml b/source/.idea/codeStyles/codeStyleConfig.xml
deleted file mode 100644
index a55e7a179bde3e4e772c29c0c85e53354aa54618..0000000000000000000000000000000000000000
--- a/source/.idea/codeStyles/codeStyleConfig.xml
+++ /dev/null
@@ -1,5 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
-  <state>
-    <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default" />
-  </state>
-</component>
\ No newline at end of file
diff --git a/source/.idea/misc.xml b/source/.idea/misc.xml
deleted file mode 100644
index 639900d13c6182e452e33a3bd638e70a0146c785..0000000000000000000000000000000000000000
--- a/source/.idea/misc.xml
+++ /dev/null
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
-  <component name="ProjectRootManager">
-    <output url="file://$PROJECT_DIR$/out" />
-  </component>
-</project>
\ No newline at end of file
diff --git a/source/.idea/modules.xml b/source/.idea/modules.xml
deleted file mode 100644
index 66f3350852f70fbfb98aa5e634317f8bf4b7bfaf..0000000000000000000000000000000000000000
--- a/source/.idea/modules.xml
+++ /dev/null
@@ -1,8 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
-  <component name="ProjectModuleManager">
-    <modules>
-      <module fileurl="file://$PROJECT_DIR$/.idea/source.iml" filepath="$PROJECT_DIR$/.idea/source.iml" />
-    </modules>
-  </component>
-</project>
\ No newline at end of file
diff --git a/source/.idea/vcs.xml b/source/.idea/vcs.xml
deleted file mode 100644
index 6c0b8635858dc7ad44b93df54b762707ce49eefc..0000000000000000000000000000000000000000
--- a/source/.idea/vcs.xml
+++ /dev/null
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
-  <component name="VcsDirectoryMappings">
-    <mapping directory="$PROJECT_DIR$/.." vcs="Git" />
-  </component>
-</project>
\ No newline at end of file
diff --git a/source/IntegrationTests/StepUntilDebug.mmt b/source/IntegrationTests/StepUntilDebug.mmt
new file mode 100644
index 0000000000000000000000000000000000000000..7c8dec75054c50ac380eef924e8d516cf5376bba
--- /dev/null
+++ b/source/IntegrationTests/StepUntilDebug.mmt
@@ -0,0 +1,11 @@
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests/stepuntildebug ❚
+
+rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
+
+import frameworld http://mathhub.info/FrameIT/frameworld ❚
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
+
+theory StepUntilDebug =
+    include ☞http://mathhub.info/FrameIT/frameworld?StepUntil ❙
+    my_list: List[ℝ] ❘ = stepUntil 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
+❚
diff --git a/source/dynamics.mmt b/source/dynamics.mmt
index 6e77c20c53534c88c9b1139f95343a6d169a8b3a..cf72a7e10fa2c6fdf115cb5a4e8e970295b5a34a 100644
--- a/source/dynamics.mmt
+++ b/source/dynamics.mmt
@@ -3,10 +3,13 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 import base http://mathhub.info/MitM/Foundation ❚
 import arith http://mathhub.info/MitM/core/arithmetics ❚
 import rules scala://rules.frameit.mmt.kwarc.info ❚
-fixmeta ?FrameworldMeta ❚
 
-theory StepUntilWrap =
-    stepUntil: ℝ ⟶ (ℝ ⟶ ℝ) ⟶ (ℝ ⟶ bool) ⟶ List[ℝ] ❘ # stepUntil 1 2 3 ❙
-    rule rules?StepUntilRule (true) ❙
+theory StepUntilRaw =
+    // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
+    stepUntil # stepUntil 1 2 3 ❙
 ❚
 
+theory StepUntil : ?FrameworldMeta =
+    include ?StepUntilRaw ❙
+    rule rules?StepUntilRule (true) ❙
+❚