--- a/src/OD.agda	Mon Jan 16 10:50:30 2023 +0900
+++ b/src/OD.agda	Mon Jan 16 14:01:45 2023 +0900
@@ -217,6 +217,9 @@
 ∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
 
+0<P→ne  : { x : HOD  } → o∅ o< & x → ¬ (  od x  == od od∅  )
+0<P→ne {x} 0<x eq = ⊥-elim ( o<¬≡ (sym (=od∅→≡o∅ eq)) 0<x )
+
 ∈∅< : { x : HOD  } {y : Ordinal } → odef x y → o∅  o< (& x)
 ∈∅<  {x} {y} d with trio< o∅ (& x)
 ... | tri< a ¬b ¬c = a