(motive : Lean.Elab.Tactic.ElabSimpArgResult → Sort u_1) →
  (arg : Lean.Elab.Tactic.ElabSimpArgResult) →
    ((entries : Array Lean.Meta.SimpEntry) → motive (Lean.Elab.Tactic.ElabSimpArgResult.addEntries entries)) →
      ((fvarId : Lean.FVarId) → motive (Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold fvarId)) →
        ((declName : Lean.Name) →
            (post : Bool) → motive (Lean.Elab.Tactic.ElabSimpArgResult.addSimproc declName post)) →
          ((origin : Lean.Meta.Origin) → motive (Lean.Elab.Tactic.ElabSimpArgResult.erase origin)) →
            ((name : Lean.Name) → motive (Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc name)) →
              ((simpExt? : Option Lean.Meta.SimpExtension) →
                  (simprocExt? : Option Lean.Meta.Simp.SimprocExtension) →
                    (h : (simpExt?.isSome || simprocExt?.isSome) = true) →
                      motive (Lean.Elab.Tactic.ElabSimpArgResult.ext simpExt? simprocExt? h)) →
                (Unit → motive Lean.Elab.Tactic.ElabSimpArgResult.star) →
                  (Unit → motive Lean.Elab.Tactic.ElabSimpArgResult.none) → motive arg