Make progress on the hashmap properties

2 files changed, 4 insertions, 4 deletions

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index b54bdf7a..6f820a84 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -81,8 +81,8 @@ section Methods
     let (fExpr, f, args) ← do
       if mf.isConst ∧ mf.constName = ``Bind.bind then do
         -- Dive into the bind
-        let fExpr := margs.get! 4
-        fExpr.consumeMData.withApp fun f args => pure (fExpr, f, args)
+        let fExpr := (margs.get! 4).consumeMData
+        fExpr.withApp fun f args => pure (fExpr, f, args)
       else pure (mExpr, mf, margs)
     trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
     if ¬ f.isConst then throwError "Not a constant: {f}"
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a281f1d2..a2c7764f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -58,9 +58,9 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     let (thBody, _) ← destEq thBody
     trace[Progress] "After splitting equality: {thBody}"
     -- There shouldn't be any existential variables in thBody
-    pure thBody
+    pure thBody.consumeMData
   -- Match the body with the target
-  trace[Progress] "Matching `{thBody}` with `{fExpr}`"
+  trace[Progress] "Matching:\n- body:\n{thBody}\n- target:\n{fExpr}"
   let ok ← isDefEq thBody fExpr
   if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}"
   let mgoal ← Tactic.getMainGoal