{n : ℕ} →
  {a : ℤ} →
    (b z : ℕ) →
      (motive : b ≤ z ∧ z < n ∧ a ≡ ↑z [ZMOD ↑n] → Sort u_1) →
        (x : b ≤ z ∧ z < n ∧ a ≡ ↑z [ZMOD ↑n]) → ((h₁ : b ≤ z) → (h₂ : z < n ∧ a ≡ ↑z [ZMOD ↑n]) → motive ⋯) → motive x