{α : Type} →
  {P : Sort u} →
    {attr : Lean.ParametricAttribute α} →
      {base : Std.HashMap Lean.Name α} →
        {attr' : Lean.ParametricAttribute α} →
          {base' : Std.HashMap Lean.Name α} →
            { attr := attr, base := base } = { attr := attr', base := base' } → (attr ≍ attr' → base ≍ base' → P) → P