diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean
index f72fc0a..0f6d80d 100644
--- a/Pantograph/Tactic/Congruence.lean
+++ b/Pantograph/Tactic/Congruence.lean
@@ -11,19 +11,19 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
   let userName := (← mvarId.getDecl).userName
 
   let u ← Meta.mkFreshLevelMVar
-  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-    .natural (userName := userName ++ `α)
-  let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default)
-    .synthetic (userName := userName ++ `f)
-  let a₁ ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `a₁)
-  let a₂ ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `a₂)
-  let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
-    .synthetic (userName := userName ++ `h)
+  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
+    (tag := userName ++ `α)
+  let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default)
+    (tag := userName ++ `f)
+  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₁)
+  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₂)
+  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
+    (tag := userName ++ `h)
   let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
-  let conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `conduit)
+  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
+    (tag := userName ++ `conduit)
   mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
   let result := [α, a₁, a₂, f,  h, conduit]
   return result.map (·.mvarId!)
@@ -39,20 +39,20 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
   let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
   let userName := (← mvarId.getDecl).userName
   let u ← Meta.mkFreshLevelMVar
-  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-    .natural (userName := userName ++ `α)
+  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
+    (tag := userName ++ `α)
   let fType := .forallE .anonymous α β .default
-  let f₁ ← Meta.mkFreshExprMVar (.some fType)
-    .synthetic (userName := userName ++ `f₁)
-  let f₂ ← Meta.mkFreshExprMVar (.some fType)
-    .synthetic (userName := userName ++ `f₂)
-  let a ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `a)
-  let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
-    .synthetic (userName := userName ++ `h)
+  let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₁)
+  let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₂)
+  let a ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a)
+  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
+    (tag := userName ++ `h)
   let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
-  let conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `conduit)
+  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
+    (tag := userName ++ `conduit)
   mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
   let result := [α, f₁, f₂, h, a, conduit]
   return result.map (·.mvarId!)
@@ -68,24 +68,24 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
   let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
   let userName := (← mvarId.getDecl).userName
   let u ← Meta.mkFreshLevelMVar
-  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-    .natural (userName := userName ++ `α)
+  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
+    (tag := userName ++ `α)
   let fType := .forallE .anonymous α β .default
-  let f₁ ← Meta.mkFreshExprMVar (.some fType)
-    .synthetic (userName := userName ++ `f₁)
-  let f₂ ← Meta.mkFreshExprMVar (.some fType)
-    .synthetic (userName := userName ++ `f₂)
-  let a₁ ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `a₁)
-  let a₂ ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `a₂)
-  let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
-    .synthetic (userName := userName ++ `h₁)
-  let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
-    .synthetic (userName := userName ++ `h₂)
+  let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₁)
+  let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₂)
+  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₁)
+  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₂)
+  let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
+    (tag := userName ++ `h₁)
+  let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
+    (tag := userName ++ `h₂)
   let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
-  let conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `conduit)
+  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
+    (tag := userName ++ `conduit)
   mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
   let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
   return result.map (·.mvarId!)
diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 2c52f12..993d287 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -66,6 +66,7 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
   mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
   let recursorType ← Meta.inferType recursor
   let resultant ← mvarId.getType
+  let tag ← mvarId.getTag
 
   let info ← match getRecursorInformation recursorType with
     | .some info => pure info
@@ -81,9 +82,9 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
       let bvarIndex := info.nArgs - i - 1
       let argGoal ← if bvarIndex = info.iMotive then
           let surrogateMotiveType ← info.surrogateMotiveType prev resultant
-          Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
+          Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive)
         else
-          Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
+          Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous)
       let prev :=  prev ++ [argGoal]
       go (i + 1) prev
     termination_by info.nArgs - i
@@ -91,7 +92,7 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
 
   -- Create the conduit type which proves the result of the motive is equal to the goal
   let conduitType ← info.conduitType newMVars resultant
-  let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
+  let goalConduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType (tag := `conduit)
   mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
   newMVars := newMVars ++ [goalConduit]
 
diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean
index 836041c..180c2f4 100644
--- a/Test/Tactic/Congruence.lean
+++ b/Test/Tactic/Congruence.lean
@@ -25,7 +25,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
     let f := newGoals.get! 3
     let h := newGoals.get! 4
     let c := newGoals.get! 5
-    let results ← f.apply (← parseSentence "List.reverse")
+    let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
     addTest $ LSpec.check "apply" (results.length = 0)
     addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
     addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")