Probably copy paste bug from the other Forall pattern, since the variables are named differently.
This is the deduction rule:

    A₀[x@n ≔ e₀] = A₁   ↑(1, y, 0, e₀) = e₁   B₀[x@n ≔ e₁] = B₁
    ───────────────────────────────────────────────────────────  ; x ≠ y
    (∀(y : A₀) → B₀)[x@n ≔ e₀] = ∀(y : A₁) → B₁

This would be caught by the alpha-normalizatifon/success/unit/FunctionTypeNestedBindingX test, when the complete testsuite is run.