Pin WF-1 Buchholz well-foundedness in smoke manifests

Author: hyperpolymath

proofs/agda/All.agda

@@ -38,6 +38,7 @@ open import Ordinal.Buchholz.Order
 open import Ordinal.Buchholz.Psi
 open import Ordinal.Buchholz.Examples
 open import Ordinal.Buchholz.WellFormed
+open import Ordinal.Buchholz.WellFounded
 open import Ordinal.Buchholz.Smoke
 
 open import Smoke

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -66,6 +66,12 @@ open import Ordinal.Buchholz.Examples using
   ; psi0-omega1-not-at-0
   )
 
+open import Ordinal.Buchholz.WellFounded using
+  ( <Ω-wf
+  ; wf-<ᵇ
+  ; <ᵇ-irreflexive
+  )
+
 open import Ordinal.Buchholz.WellFormed using
   ( WfΩ
   ; WfBT

proofs/agda/Smoke.agda

@@ -207,6 +207,12 @@ open import Ordinal.Buchholz.Examples using
   ; psi0-omega1-not-at-0
   )
 
+open import Ordinal.Buchholz.WellFounded using
+  ( <Ω-wf
+  ; wf-<ᵇ
+  ; <ᵇ-irreflexive
+  )
+
 open import Ordinal.Buchholz.Smoke using ()
 
 open import Ordinal.Buchholz.WellFormed using