Fix another infinite lookup

Author: Negabinary

src/language/term/Equality.re

@@ -295,7 +295,11 @@ let equality =
       open OptUtil.Syntax;
       let lookup1 = {
         let* env1 = env1;
-        Environment.lookup(env1, x);
+        let v = Environment.lookup(env1, x);
+        switch (v) {
+        | Some({term: Var(v), _}) when v == x => None
+        | _ => v
+        };
       };
       switch (lookup1) {
       | Some(v1) => exp'(v1, e2)
@@ -309,7 +313,11 @@ let equality =
       open OptUtil.Syntax;
       let lookup2 = {
         let* env2 = env2;
-        Environment.lookup(env2, y);
+        let v = Environment.lookup(env2, y);
+        switch (v) {
+        | Some({term: Var(v), _}) when v == y => None
+        | _ => v
+        };
       };
       switch (lookup2) {
       | Some(v2) => exp'(e1, v2)

src/web/app/editors/stepper/MissingStep.re

@@ -289,9 +289,16 @@ module Update = {
           |> {
             let.calc sctx = ctx
             and.calc to_exp = cached_exp
-            and.calc from_exp = exp;
+            and.calc from_exp = selected_exp;
             let env = SemanticCtx.get_env(sctx);
-            let from_exp = Substitution.in_exp(env, from_exp);
+            let from_exp =
+              Substitution.in_exp(
+                env,
+                from_exp
+                |> Option.value(
+                     ~default=IdTagged.FreshGrammar.Exp.empty_hole(),
+                   ),
+              );
             let to_exp = Substitution.in_exp(env, to_exp);
             RewriteChecker.check_rewrite(~settings, ~env, from_exp, to_exp);
           };
@@ -325,9 +332,16 @@ module Update = {
           |> {
             let.calc sctx = ctx
             and.calc to_exp = cached_exp
-            and.calc from_exp = exp;
+            and.calc from_exp = selected_exp;
             let env = SemanticCtx.get_env(sctx);
-            let from_exp = Substitution.in_exp(env, from_exp);
+            let from_exp =
+              Substitution.in_exp(
+                env,
+                from_exp
+                |> Option.value(
+                     ~default=IdTagged.FreshGrammar.Exp.empty_hole(),
+                   ),
+              );
             let to_exp = Substitution.in_exp(env, to_exp);
             RewriteChecker.check_written_step(
               ~settings,