{motive : Simps.ParsedProjectionData → Sort u} →
  (t : Simps.ParsedProjectionData) →
    ((strName : Lean.Name) →
        (strStx : Lean.Syntax) →
          (newName : Lean.Name) →
            (newStx : Lean.Syntax) →
              (isDefault isPrefix : Bool) →
                (expr? : Option Lean.Expr) →
                  (projNrs : Array ℕ) →
                    (isCustom : Bool) →
                      motive
                        { strName := strName, strStx := strStx, newName := newName, newStx := newStx,
                          isDefault := isDefault, isPrefix := isPrefix, expr? := expr?, projNrs := projNrs,
                          isCustom := isCustom }) →
      motive t