{α : Type} →
  {motive : Lean.ParametricAttributeImpl α → Sort u} →
    (t : Lean.ParametricAttributeImpl α) →
      ((toAttributeImplCore : Lean.AttributeImplCore) →
          (getParam : Lean.Name → Lean.Syntax → Lean.AttrM α) →
            (afterSet : Lean.Name → α → Lean.AttrM Unit) →
              (preserveOrder : Bool) →
                (filterExport : Lean.Environment → Lean.Name → α → Bool) →
                  motive
                    { toAttributeImplCore := toAttributeImplCore, getParam := getParam, afterSet := afterSet,
                      preserveOrder := preserveOrder, filterExport := filterExport }) →
        motive t