{P : Sort u} →
  {mvarId : Lean.MVarId} →
    {newEqs : Array Lean.FVarId} →
      {remainingNames : List Lean.Name} →
        {mvarId' : Lean.MVarId} →
          {newEqs' : Array Lean.FVarId} →
            {remainingNames' : List Lean.Name} →
              Lean.Meta.InjectionResult.subgoal mvarId newEqs remainingNames =
                  Lean.Meta.InjectionResult.subgoal mvarId' newEqs' remainingNames' →
                (mvarId = mvarId' → newEqs = newEqs' → remainingNames = remainingNames' → P) → P