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

Single-line fix to Slice 2-bplus's `ω-rank-pow-mono-≤Ω` — the ω≤ω
case used `≤′-refl` without an explicit `{α}` annotation, leaving
the implicit unconstrained.  Fix: `≤′-refl {ω-rank-pow ω}`.

Surfaced after installing agda 2.6.3 + stdlib v2.3 locally in the
container.  Original PR #133 had merged unverified because the
container had no agda binary AND GitHub Actions quota was exhausted
(CI checks stuck in "queued" indefinitely).

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

Admin-merged before CI green (quota issue ongoing).

Author: hyperpolymath

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`