∀ {motive : Lean.Expr → Sort u} (t : Lean.Expr)
  (forallE :
    (binderName : Lean.Name) →
      (binderType body : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName binderType body binderInfo))
  («else» : Nat.hasNotBit 128 t.ctorIdx → motive t) (h : Nat.hasNotBit 128 t.ctorIdx),
  Lean.Meta.IndPredBelow.toImplicit._sparseCasesOn_1✝ t forallE «else» = «else» h