{motive : Lean.Elab.CompletionInfo → Sort u} →
  (t : Lean.Elab.CompletionInfo) →
    ((stx : Lean.Syntax) →
        (id : Lean.Name) →
          (danglingDot : Bool) →
            (lctx : Lean.LocalContext) →
              (expectedType? : Option Lean.Expr) →
                motive (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType?)) →
      ((termInfo : Lean.Elab.TermInfo) →
          (expectedType? : Option Lean.Expr) → motive (Lean.Elab.CompletionInfo.dot termInfo expectedType?)) →
        ((stx : Lean.Syntax) →
            (id : Lean.Name) →
              (lctx : Lean.LocalContext) →
                (expectedType? : Option Lean.Expr) →
                  motive (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType?)) →
          ((stx : Lean.Syntax) →
              (id : Option Lean.Name) →
                (lctx : Lean.LocalContext) →
                  (structName : Lean.Name) → motive (Lean.Elab.CompletionInfo.fieldId stx id lctx structName)) →
            ((stx : Lean.Syntax) → motive (Lean.Elab.CompletionInfo.option stx)) →
              ((stx partialId : Lean.Syntax) → motive (Lean.Elab.CompletionInfo.errorName stx partialId)) →
                ((stx : Lean.Syntax) →
                    (id? : Option Lean.Name) →
                      (danglingDot : Bool) →
                        (scopeNames : List String) →
                          motive (Lean.Elab.CompletionInfo.endSection stx id? danglingDot scopeNames)) →
                  ((stx : Lean.Syntax) → motive (Lean.Elab.CompletionInfo.tactic stx)) →
                    (Nat.hasNotBit 495 t.ctorIdx → motive t) → motive t