{P : Sort u} →
  {goal : Lean.MVarId} →
    {mvars : Std.HashSet Lean.MVarId} →
      {goal' : Lean.MVarId} →
        {mvars' : Std.HashSet Lean.MVarId} →
          { goal := goal, mvars := mvars } = { goal := goal', mvars := mvars' } →
            (goal = goal' → mvars = mvars' → P) → P