ordinal(buchholz): fix Slice 2-bplus — explicit implicit on ≤′-refl

PR #133's `rank-pow-dominated-by-head-Ω` was unverified at merge time:
the container had no agda binary, CI was queue-stuck because the
GitHub Actions quota was exhausted, and verification had been by
inspection only.  Installing agda 2.6.3 + stdlib v2.3 in the container
revealed a single inference miss:

  ω-rank-pow-mono-≤Ω ω≤ω = ≤′-refl

leaves the implicit {α} of ≤′-refl unconstrained — Agda can't determine
whether to return the `oz`, `osuc`, or `olim` clause's witness.  The
fix is the explicit annotation `≤′-refl {ω-rank-pow ω}`.

`agda -i proofs/agda proofs/agda/All.agda` exits 0 with this fix.

Honest provenance: the rest of the Slice 2-bplus content was correct
as-inspected (the structural recursion, the additive-principal
closure at the ω branch, the rank-y-bound helper).  Only this one
case had a real type-inference gap.

https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S

Author: claude

proofs/agda/Ordinal/Buchholz/RankPowDomination.agda

@@ -166,7 +166,7 @@ open import Ordinal.Buchholz.RankPow using
 ω-rank-pow-mono-≤Ω : ∀ {μ ν} → μ ≤Ω ν → ω-rank-pow μ ≤′ ω-rank-pow ν
 ω-rank-pow-mono-≤Ω (fin≤fin m≤n) = ω^-mono-≤ (s≤s m≤n)
 ω-rank-pow-mono-≤Ω {fin m} fin≤ω = f-in-lim′ (λ k → ω^ (suc k)) m
-ω-rank-pow-mono-≤Ω ω≤ω           = ≤′-refl
+ω-rank-pow-mono-≤Ω ω≤ω           = ≤′-refl {ω-rank-pow ω}
 
 ----------------------------------------------------------------------
 -- Positivity of `ω-rank-pow-succ`