∀ {mvarId : Lean.MVarId} {ref : Lean.Syntax} {kind : Lean.Elab.Term.MVarErrorKind} {mvarId_1 : Lean.MVarId}
  {ref_1 : Lean.Syntax} {kind_1 : Lean.Elab.Term.MVarErrorKind},
  { mvarId := mvarId, ref := ref, kind := kind } = { mvarId := mvarId_1, ref := ref_1, kind := kind_1 } →
    mvarId = mvarId_1 ∧ ref = ref_1 ∧ kind = kind_1