--- a/src/OD.agda	Fri Aug 19 10:08:14 2022 +0900
+++ b/src/OD.agda	Mon Aug 22 07:39:18 2022 +0900
@@ -120,7 +120,7 @@
 
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
-¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
+¬OD-order & * c<→o< = o≤> <-osuc (c<→o< {Ords} OneObj )
 
 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup
 ¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥