diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 8f890e3..63331af 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -70,11 +70,10 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
         let pending ← mvarIdPending.withContext do
           let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
           --IO.println s!"{padding}├Pre: {inner}"
-          let r := (← Expr.abstractM inner fvars).instantiateRev args
-          pure r
+          pure <| (← inner.abstractM fvars).instantiateRev args
 
         -- Tail arguments
-        let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray)
+        let result := mkAppRange pending fvars.size args.size args
         --IO.println s!"{padding}├MD {result}"
         return .done result
       else
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index e0625e8..d3df45f 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -212,11 +212,10 @@ inductive TacticExecute where
 def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult :=
   runTermElabM do
     state.restoreElabM
-    let tactic := match tacticExecute with
+    state.execute goalId $ match tacticExecute with
       | .congruenceArg => Tactic.congruenceArg
       | .congruenceFun => Tactic.congruenceFun
       | .congruence => Tactic.congruence
-    state.execute goalId tactic