{m : Type → Type} →
  {motive : Lean.Elab.MonadAutoImplicits m → Sort u} →
    (t : Lean.Elab.MonadAutoImplicits m) →
      ((getAutoImplicits : m (Array Lean.Expr)) → motive { getAutoImplicits := getAutoImplicits }) → motive t