Pin smoke imports to +/psiω and +/psifin names

hyperpolymath · hyperpolymath · commit dd291a6ed5a6 · 2026-04-23T00:23:58.000+01:00
diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda
@@ -56,13 +56,14 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
   ; <ᵇ-+ω
+  ; <ᵇ-+ψω
   ; <ᵇ-+1
   ; <ᵇ-irrefl
   ; <ᵇ-trans
   ; <ᵇ-inv-Ω+
   ; <ᵇ-inv-+Ωfin
   ; <ᵇ-inv-ψ+
-  ; <ᵇ-inv-+ψ
+  ; <ᵇ-inv-+ψfin
   )
 
 open import Ordinal.Buchholz.Psi using
diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda
@@ -183,13 +183,14 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
   ; <ᵇ-+ω
+  ; <ᵇ-+ψω
   ; <ᵇ-+1
   ; <ᵇ-irrefl
   ; <ᵇ-trans
   ; <ᵇ-inv-Ω+
   ; <ᵇ-inv-+Ωfin
   ; <ᵇ-inv-ψ+
-  ; <ᵇ-inv-+ψ
+  ; <ᵇ-inv-+ψfin
   ; bzero<Ω0
   ; Ω0<Ω1
   ; Ω1<Ωω
