Artificial intelligent assistant

In natural deduction, may a sequent we want to prove have another sequent as its premise? For example can we have something like $(A\vdash B)\vdash C$ to prove in natural deduction? I've seen a single sequent this shape somewhere (don't remember where it was or if it was about natural deduction at all though!)

Usually not. $\vdash$ expects a list (or set) of (object-level) propositions and a proposition and $(A\vdash B)$ is not a(n object-level) proposition. That is, it's not a formula of the object language. This is almost always the case. There are systems of nested sequents (e.g.) that do allow things like this, but they are unusual.

xcX3v84RxoQ-4GxG32940ukFUIEgYdPy fae3ebabd8a879d4b80d00eefddb96c6