Further fixes to duplicate variable names. (#131)

Smt/Reconstruct.lean

@@ -16,6 +16,7 @@ open Lean
 open Attribute
 
 structure Reconstruct.state where
+  userNames : HashMap String FVarId
   termCache : HashMap cvc5.Term Expr
   proofCache : HashMap cvc5.Proof Expr
   count : Nat
@@ -62,9 +63,10 @@ def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : Reconstru
     | .error _ => m!"{bombEmoji}"
 
 def withNewTermCache (k : ReconstructM α) : ReconstructM α := do
-  let state ← get
+  let termCache := (← get).termCache
+  modify fun state => { state with termCache := {} }
   let r ← k
-  set { ← get with termCache := state.termCache }
+  modify fun state => { state with termCache := termCache }
   return r
 
 def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t => do
@@ -89,9 +91,10 @@ where
     throwError "Failed to reconstruct term {t} with kind {t.getKind}"
 
 def withNewProofCache (k : ReconstructM α) : ReconstructM α := do
-  let state ← get
+  let proofCache := (← get).proofCache
+  modify fun state => { state with proofCache := {} }
   let r ← k
-  set { ← get with proofCache := state.proofCache }
+  modify fun state => { state with proofCache := proofCache }
   return r
 
 def withProofCache (r : cvc5.Proof → ReconstructM Expr) (pf : cvc5.Proof) : ReconstructM Expr := do
@@ -172,10 +175,10 @@ def traceReconstructProof (r : Except Exception (Expr × Expr × List MVarId)) :
   | _     => m!"{bombEmoji}"
 
 open Qq in
-partial def reconstructProof (pf : cvc5.Proof) : MetaM (Expr × Expr × List MVarId) := do
+partial def reconstructProof (pf : cvc5.Proof) (fvNames : HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do
   withTraceNode `smt.reconstruct.proof traceReconstructProof do
-  let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨{}, {}, 0, #[], #[]⟩
-  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
+  let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨fvNames, {}, {}, 0, #[], #[]⟩
+  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
   return (p, q($h trivial), mvs.toList)
 
 open cvc5 in
@@ -217,10 +220,15 @@ open Lean.Elab Tactic in
     match r with
       | .error e => logInfo (repr e)
       | .ok pf =>
-        let (p, hp, mvs) ← reconstructProof pf
+        let (p, hp, mvs) ← reconstructProof pf (← getFVarNames)
         let mv ← Tactic.getMainGoal
         let mv ← mv.assert (Name.num `s 0) p hp
         let (_, mv) ← mv.intro1
         replaceMainGoal (mv :: mvs)
+where
+  getFVarNames : MetaM (HashMap String FVarId) := do
+    let lCtx ← getLCtx
+    return lCtx.getFVarIds.foldl (init := {}) fun m fvarId =>
+      m.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId
 
 end Smt

Smt/Reconstruct/Builtin.lean

@@ -29,16 +29,18 @@ def getFVarExpr! (n : Name) : MetaM Expr := do
   | some d => return d.toExpr
   | none   => throwError "unknown free variable '{n}'"
 
-def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   =>
-    let c ← getConstInfo n
-    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
+  match (← get).userNames.find? n with
+  | some fv => return .fvar fv
+  | none   => match (← getLCtx).findFromUserName? n.toName with
+    | some d => return d.toExpr
+    | none   =>
+      let c ← getConstInfo n.toName
+      return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
 
 @[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
   | .VARIABLE => getFVarExpr! (getVariableName t)
-  | .CONSTANT => getFVarOrConstExpr! (Name.mkSimple t.getSymbol)
+  | .CONSTANT => getFVarOrConstExpr! t.getSymbol
   | .EQUAL =>
     let α : Q(Type) ← reconstructSort t[0]!.getSort
     let x : Q($α) ← reconstructTerm t[0]!
@@ -65,7 +67,12 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
   | _ => return none
 where
   getVariableName (t : cvc5.Term) : Name :=
-    if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId
+    if t.hasSymbol then
+      if t.getSymbol.toName == .anonymous then
+        Name.mkSimple t.getSymbol
+      else
+        t.getSymbol.toName
+    else Name.num `x t.getId
 
 def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   match pf.getRewriteRule with

Smt/Reconstruct/Quant.lean

@@ -28,7 +28,12 @@ namespace Smt.Reconstruct.Quant
 open Lean Qq
 
 def getVariableName (t : cvc5.Term) : Name :=
-  if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId
+  if t.hasSymbol then
+    if t.getSymbol.toName == .anonymous then
+      Name.mkSimple t.getSymbol
+    else
+      t.getSymbol.toName
+  else Name.num `x t.getId
 
 @[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with
   | .FORALL =>
@@ -223,8 +228,8 @@ where
       xs.foldrM f (p, q, h)
     addThm q($p = $q) h
   reconstructSkolemize (pf : cvc5.Proof) : ReconstructM Expr := do
-    let res := pf.getChildren[0]!.getResult
-    let es ← reconstructQuant.reconstructForallSkolems res[0]! (res[0]![0]!.getNumChildren - 1)
+    let chRes := pf.getChildren[0]!.getResult
+    let es ← reconstructQuant.reconstructForallSkolems chRes[0]! (chRes[0]![0]!.getNumChildren - 1)
     let f := fun h e => do
       let α : Q(Type) ← pure (e.getArg! 0)
       let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)

Smt/Reconstruct/UF.lean

@@ -13,16 +13,18 @@ namespace Smt.Reconstruct.UF
 
 open Lean Qq
 
-def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   =>
-    let c ← getConstInfo n
-    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
+  match (← get).userNames.find? n with
+  | some fv => return .fvar fv
+  | none   => match (← getLCtx).findFromUserName? n.toName with
+    | some d => return d.toExpr
+    | none   =>
+      let c ← getConstInfo n.toName
+      return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
 
 @[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with
   | .INTERNAL_SORT_KIND
-  | .UNINTERPRETED_SORT => getFVarOrConstExpr! (Name.mkSimple s.getSymbol)
+  | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol
   | _ => return none
 
 @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with

Smt/Tactic/Smt.lean

@@ -20,10 +20,19 @@ open Lean hiding Command
 open Elab Tactic Qq
 open Smt Translate Query Reconstruct Util
 
-def prepareSmtQuery (hs : List Expr) (goalType : Expr) : MetaM (List Command) := do
+def genUniqueFVarNames : MetaM (HashMap FVarId String × HashMap String FVarId) := do
+  let lCtx ← getLCtx
+  let st : NameSanitizerState := { options := {}}
+  let (lCtx, _) := (lCtx.sanitizeNames st).run
+  return lCtx.getFVarIds.foldl (init := ({}, {})) fun (m₁, m₂) fvarId =>
+    let m₁ := m₁.insert fvarId (lCtx.getRoundtrippingUserName? fvarId).get!.toString
+    let m₂ := m₂.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId
+    (m₁, m₂)
+
+def prepareSmtQuery (hs : List Expr) (goalType : Expr) (fvNames : HashMap FVarId String) : MetaM (List Command) := do
   let goalId ← Lean.mkFreshMVarId
   Lean.Meta.withLocalDeclD goalId.name (mkNot goalType) fun g =>
-  Query.generateQuery g hs
+  Query.generateQuery g hs fvNames
 
 def withProcessedHints (mv : MVarId) (hs : List Expr) (k : MVarId → List Expr → MetaM α): MetaM α :=
   go mv hs [] k
@@ -46,7 +55,8 @@ def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (L
   mv.withContext do
   let goalType : Q(Prop) ← mv.getType
   -- 2. Generate the SMT query.
-  let cmds ← prepareSmtQuery hs (← mv.getType)
+  let (fvNames₁, fvNames₂) ← genUniqueFVarNames
+  let cmds ← prepareSmtQuery hs (← mv.getType) fvNames₁
   let cmds := .setLogic "ALL" :: cmds
   trace[smt] "goal: {goalType}"
   trace[smt] "\nquery:\n{Command.cmdsAsQuery (cmds ++ [.checkSat])}"
@@ -61,7 +71,7 @@ def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (L
     throwError "unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]`"
   | .ok pf =>
     -- 4b. Reconstruct proof.
-    let (p, hp, mvs) ← reconstructProof pf
+    let (p, hp, mvs) ← reconstructProof pf fvNames₂
     let mv ← mv.assert (← mkFreshId) p hp
     let ⟨_, mv⟩ ← mv.intro1
     let ts ← hs.mapM Meta.inferType
@@ -130,7 +140,7 @@ def parseTimeout : TSyntax `smtTimeout → TacticM (Option Nat)
   let (hs, mv) ← Preprocess.elimIff mv hs
   mv.withContext do
   let goalType ← mv.getType
-  let cmds ← prepareSmtQuery hs (← mv.getType)
+  let cmds ← prepareSmtQuery hs (← mv.getType) (← genUniqueFVarNames).fst
   let cmds := cmds ++ [.checkSat]
   logInfo m!"goal: {goalType}\n\nquery:\n{Command.cmdsAsQuery cmds}"
 

Smt/Translate.lean

@@ -45,6 +45,8 @@ structure TranslationM.State where
   /-- A mapping from a scopped name to a suffix index that makes it unique. This field does not handle
   scopping, which should be handled by `withScopedName` -/
   scopedNames : HashMap Name Nat := .empty
+  /-- A mapping from fvars to unique names. -/
+  uniqueFVarNames : HashMap FVarId String := .empty
 
 abbrev TranslationM := StateT TranslationM.State MetaM
 
@@ -137,9 +139,13 @@ partial def applyTranslators? : Translator := withCache fun e => do
       -- Then try splitting subexpressions
       match e with
       | fvar fv =>
-        if !(← get).localFVars.contains fv then
+        if (← get).localFVars.contains fv then
+          return symbolT (← fv.getUserName).toString
+        else
           modify fun st => { st with depFVars := st.depFVars.insert fv }
-        return symbolT (← fv.getUserName).toString
+          match (← get).uniqueFVarNames.find? fv with
+          | some n => return symbolT n
+          | none   => return symbolT (← fv.getUserName).toString
       | const nm _ =>
         modify fun st => { st with depConstants := st.depConstants.insert nm }
         return symbolT nm.toString

Smt/Translate/Query.lean

@@ -158,7 +158,10 @@ def addCommandFor (e tp : Expr) : QueryBuilderM (Array Expr) := do
 
   -- Otherwise it is a local/global declaration with name `nm`.
   let nm ← match e with
-    | fvar id .. => pure (← id.getDecl).userName.toString
+    | fvar id .. =>
+      match (← (get : TranslationM _)).uniqueFVarNames.find? id with
+      | some nm => pure nm
+      | none    => pure (← id.getUserName).toString
     | const n .. => pure n.toString
     | _          => throwError "internal error, expected fvar or const but got{indentD e}\nof kind {e.ctorName}"
 
@@ -253,14 +256,14 @@ def emitVertex (cmds : HashMap Expr Command) (e : Expr) : StateT (List Command)
   let some cmd := cmds.find? e | throwError "no command was computed for {e}"
   set (← addCommand cmd (← get))
 
-def generateQuery (goal : Expr) (hs : List Expr) : MetaM (List Command) :=
+def generateQuery (goal : Expr) (hs : List Expr) (fvNames : HashMap FVarId String) : MetaM (List Command) :=
   withTraceNode `smt.translate.query (fun _ => pure .nil) do
     trace[smt.translate.query] "Goal: {← inferType goal}"
     trace[smt.translate.query] "Provided Hints: {hs}"
     let ((_, st), _) ← QueryBuilderM.buildDependencyGraph goal
       |>.run { toDefine := hs : QueryBuilderM.Config }
       |>.run { : QueryBuilderM.State }
-      |>.run { : TranslationM.State }
+      |>.run { uniqueFVarNames := fvNames : TranslationM.State }
     trace[smt.translate.query] "Dependency Graph: {st.graph}"
     -- The type of the proof generated by a solver depends on the order of asserions. We assert the
     -- Lean goal at the end of the query to simplify unification during proof reconstruction.

Test/EUF/Issue126.expected

@@ -1,86 +1 @@
-goal: ¬b n →
-  te n o r v → (∃ q, nm q ∧ ∀ (s : a), nmm s q → tb s n o r v) ∨ ∃ q, ngt q ∧ ∀ (s : a), nmm s q → tc s n o r v
-
-query:
-(declare-sort n 0)
-(declare-fun ngt (n) Bool)
-(declare-fun ne (n) Bool)
-(assert (forall ((s n)) (=> (ngt s) (not (ne s)))))
-(declare-fun nm (n) Bool)
-(assert (forall ((s n)) (=> (nm s) (ngt s))))
-(declare-sort a 0)
-(declare-fun nmm (a n) Bool)
-(declare-fun b (a) Bool)
-(assert (forall ((s n)) (=> (ngt s) (exists ((a a)) (and (nmm a s) (not (b a)))))))
-(assert (forall ((s1 n)) (forall ((s2 n)) (exists ((a a)) (and (nmm a s1) (and (nmm a s2) (not (b a))))))))
-(declare-sort v 0)
-(declare-sort r 0)
-(declare-fun ta (a a r v) Bool)
-(declare-fun tf (a a r v) Bool)
-(declare-fun sd (a a r v) Bool)
-(declare-fun sb (a a a r v) Bool)
-(declare-fun sc (a a a r v) Bool)
-(declare-fun tc (a a a r v) Bool)
-(declare-fun se (a a r v) Bool)
-(declare-fun sg (a r) Bool)
-(declare-fun sa (a a r v) Bool)
-(declare-fun td (a a r v) Bool)
-(declare-fun tb (a a a r v) Bool)
-(declare-fun te (a a r v) Bool)
-(declare-fun tg (a r) Bool)
-(declare-fun sf (a a r v) Bool)
-(assert (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (or (and (not (b s)) (= (sa s d r v) (ta s d r v))) (and (b s) (=> (sa s d r v) (ta s d r v)))))))) (and (forall ((s a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (or (and (not (b s)) (= (sb s d o r v) (tb s d o r v))) (and (b s) (=> (sb s d o r v) (tb s d o r v))))))))) (and (forall ((s a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (or (and (not (b s)) (= (sc s d o r v) (tc s d o r v))) (and (b s) (=> (sc s d o r v) (tc s d o r v))))))))) (and (forall ((a_2 a)) (forall ((a_3 r)) (= (sg a_2 a_3) (tg a_2 a_3)))) (and (forall ((a_2 a)) (forall ((a_3 a)) (forall ((a_4 r)) (forall ((a_5 v)) (= (sd a_2 a_3 a_4 a_5) (td a_2 a_3 a_4 a_5)))))) (and (forall ((a_2 a)) (forall ((a_3 a)) (forall ((a_4 r)) (forall ((a_5 v)) (= (se a_2 a_3 a_4 a_5) (te a_2 a_3 a_4 a_5)))))) (forall ((a_2 a)) (forall ((a_3 a)) (forall ((a_4 r)) (forall ((a_5 v)) (= (sf a_2 a_3 a_4 a_5) (tf a_2 a_3 a_4 a_5)))))))))))))
-(assert (and (forall ((s a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (and (not (b |d₁|)) (and (not (b |d₂|)) (and (sf |d₁| s r |v₁|) (sf |d₂| s r |v₂|)))) (= |v₁| |v₂|)))))))) (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (=> (and (not (b s)) (and (not (b d)) (sf d s r v))) (and (sg s r) (forall ((d a)) (sa s d r v)))))))) (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (=> (and (not (b s)) (and (not (b d)) (se d s r v))) (and (sg s r) (forall ((d a)) (sa s d r v)))))))) (and (forall ((s a)) (forall ((o a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (not (b s)) (=> (and (sc s |d₁| o r |v₁|) (sc s |d₂| o r |v₂|)) (= |v₁| |v₂|)))))))))) (and (forall ((s a)) (forall ((o a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (not (b s)) (=> (and (sb s |d₁| o r |v₁|) (sb s |d₂| o r |v₂|)) (= |v₁| |v₂|)))))))))) (and (forall ((s a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (not (b s)) (=> (and (sa s |d₁| r |v₁|) (sa s |d₂| r |v₂|)) (= |v₁| |v₂|))))))))) (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (=> (not (b s)) (= (forall ((d a)) (sa s d r v)) (sa s d r v))))))) (and (forall ((n_1 a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n_1)) (=> (sf n_1 o r v) (exists ((q n)) (and (nm q) (forall ((s a)) (=> (nmm s q) (sc s n_1 o r v))))))))))) (and (forall ((n_1 a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n_1)) (=> (se n_1 o r v) (or (exists ((q n)) (and (nm q) (forall ((s a)) (=> (nmm s q) (sb s n_1 o r v))))) (exists ((q n)) (and (ngt q) (forall ((s a)) (=> (nmm s q) (sc s n_1 o r v)))))))))))) (and (forall ((n a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n)) (= (se n o r v) (sc n d o r v)))))))) (and (forall ((n a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n)) (=> (sd n o r v) (sa o n r v))))))) (and (forall ((n a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n)) (= (sd n o r v) (sb n d o r v)))))))) (forall ((s a)) (forall ((r r)) (=> (not (b s)) (= (sg s r) (exists ((v v)) (forall ((d a)) (sa s d r v))))))))))))))))))))
-(declare-const v v)
-(declare-const o a)
-(declare-const n a)
-(declare-const r r)
-(assert (not (=> (not (b n)) (=> (te n o r v) (or (exists ((q n)) (and (nm q) (forall ((s a)) (=> (nmm s q) (tb s n o r v))))) (exists ((q n)) (and (ngt q) (forall ((s a)) (=> (nmm s q) (tc s n o r v))))))))))
-(check-sat)
-Test/EUF/Issue126.lean:77:55: error: unsolved goals
-n✝ a r✝ v✝ : Type
-b : a → Prop
-nmm : a → n✝ → Prop
-ne ngt nm : n✝ → Prop
-nsih : ∀ (s1 s2 : n✝), ∃ a, nmm a s1 ∧ nmm a s2 ∧ ¬b a
-noh : ∀ (s : n✝), ngt s → ∃ a, nmm a s ∧ ¬b a
-nsg : ∀ (s : n✝), nm s → ngt s
-nne : ∀ (s : n✝), ngt s → ¬ne s
-sa : a → a → r✝ → v✝ → Prop
-sb sc : a → a → a → r✝ → v✝ → Prop
-sg : a → r✝ → Prop
-sd se sf : a → a → r✝ → v✝ → Prop
-ha :
-  (∀ (s d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b d₁ ∧ ¬b d₂ ∧ sf d₁ s r v₁ ∧ sf d₂ s r v₂ → v₁ = v₂) ∧
-    (∀ (s d : a) (r : r✝) (v : v✝), ¬b s ∧ ¬b d ∧ sf d s r v → sg s r ∧ ∀ (d : a), sa s d r v) ∧
-      (∀ (s d : a) (r : r✝) (v : v✝), ¬b s ∧ ¬b d ∧ se d s r v → sg s r ∧ ∀ (d : a), sa s d r v) ∧
-        (∀ (s o d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b s → sc s d₁ o r v₁ ∧ sc s d₂ o r v₂ → v₁ = v₂) ∧
-          (∀ (s o d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b s → sb s d₁ o r v₁ ∧ sb s d₂ o r v₂ → v₁ = v₂) ∧
-            (∀ (s d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b s → sa s d₁ r v₁ ∧ sa s d₂ r v₂ → v₁ = v₂) ∧
-              (∀ (s d : a) (r : r✝) (v : v✝), ¬b s → ((∀ (d : a), sa s d r v) ↔ sa s d r v)) ∧
-                (∀ (n o : a) (r : r✝) (v : v✝), ¬b n → sf n o r v → ∃ q, nm q ∧ ∀ (s : a), nmm s q → sc s n o r v) ∧
-                  (∀ (n o : a) (r : r✝) (v : v✝),
-                      ¬b n →
-                        se n o r v →
-                          (∃ q, nm q ∧ ∀ (s : a), nmm s q → sb s n o r v) ∨
-                            ∃ q, ngt q ∧ ∀ (s : a), nmm s q → sc s n o r v) ∧
-                    (∀ (n d o : a) (r : r✝) (v : v✝), ¬b n → (se n o r v ↔ sc n d o r v)) ∧
-                      (∀ (n o : a) (r : r✝) (v : v✝), ¬b n → sd n o r v → sa o n r v) ∧
-                        (∀ (n d o : a) (r : r✝) (v : v✝), ¬b n → (sd n o r v ↔ sb n d o r v)) ∧
-                          ∀ (s : a) (r : r✝), ¬b s → (sg s r ↔ ∃ v, ∀ (d : a), sa s d r v)
-ta : a → a → r✝ → v✝ → Prop
-tb tc : a → a → a → r✝ → v✝ → Prop
-tg : a → r✝ → Prop
-td te tf : a → a → r✝ → v✝ → Prop
-hb :
-  (∀ (s d : a) (r : r✝) (v : v✝), ¬b s ∧ (sa s d r v ↔ ta s d r v) ∨ b s ∧ (sa s d r v → ta s d r v)) ∧
-    (∀ (s d o : a) (r : r✝) (v : v✝), ¬b s ∧ (sb s d o r v ↔ tb s d o r v) ∨ b s ∧ (sb s d o r v → tb s d o r v)) ∧
-      (∀ (s d o : a) (r : r✝) (v : v✝), ¬b s ∧ (sc s d o r v ↔ tc s d o r v) ∨ b s ∧ (sc s d o r v → tc s d o r v)) ∧
-        (∀ (a_2 : a) (a_3 : r✝), sg a_2 a_3 = tg a_2 a_3) ∧
-          (∀ (a_2 a_3 : a) (a_4 : r✝) (a_5 : v✝), sd a_2 a_3 a_4 a_5 = td a_2 a_3 a_4 a_5) ∧
-            (∀ (a_2 a_3 : a) (a_4 : r✝) (a_5 : v✝), se a_2 a_3 a_4 a_5 = te a_2 a_3 a_4 a_5) ∧
-              ∀ (a_2 a_3 : a) (a_4 : r✝) (a_5 : v✝), sf a_2 a_3 a_4 a_5 = tf a_2 a_3 a_4 a_5
-n o : a
-r : r✝
-v : v✝
-⊢ ¬b n → te n o r v → (∃ q, nm q ∧ ∀ (s : a), nmm s q → tb s n o r v) ∨ ∃ q, ngt q ∧ ∀ (s : a), nmm s q → tc s n o r v
+Test/EUF/Issue126.lean:3:8: warning: declaration uses 'sorry'