∀ (mvarId : Lean.MVarId) (fields : Array Lean.Expr) (subst : Lean.Meta.FVarSubst) (mvarId_1 : Lean.MVarId)
  (fields_1 : Array Lean.Expr) (subst_1 : Lean.Meta.FVarSubst),
  ({ mvarId := mvarId, fields := fields, subst := subst } =
      { mvarId := mvarId_1, fields := fields_1, subst := subst_1 }) =
    (mvarId = mvarId_1 ∧ fields = fields_1 ∧ subst = subst_1)