--- a/OD.agda	Tue Jun 23 15:12:43 2020 +0900
+++ b/OD.agda	Wed Jun 24 14:05:38 2020 +0900
@@ -96,6 +96,11 @@
 maxod : {x : OD} → od→ord x o< od→ord Ords
 maxod {x} = c<→o< OneObj
 
+-- we have to avoid this contradiction
+
+bad-bad : ⊥
+bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj)
+
 -- Ordinal in OD ( and ZFSet ) Transitive Set
 Ord : ( a : Ordinal  ) → OD 
 Ord  a = record { def = λ y → y o< a }