{P : Sort u} →
  {binderName : Lean.Name} →
    {binderInfo : Lean.BinderInfo} →
      {u v : Lean.Level} →
        {binderName' : Lean.Name} →
          {binderInfo' : Lean.BinderInfo} →
            {u' v' : Lean.Level} →
              { binderName := binderName, binderInfo := binderInfo, u := u, v := v } =
                  { binderName := binderName', binderInfo := binderInfo', u := u', v := v' } →
                (binderName = binderName' → binderInfo = binderInfo' → u = u' → v = v' → P) → P