∀ {termInfo : Lean.Elab.TermInfo} {expectedType? : Option Lean.Expr} {termInfo_1 : Lean.Elab.TermInfo}
  {expectedType?_1 : Option Lean.Expr},
  Lean.Elab.CompletionInfo.dot termInfo expectedType? = Lean.Elab.CompletionInfo.dot termInfo_1 expectedType?_1 →
    termInfo = termInfo_1 ∧ expectedType? = expectedType?_1