# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562577993 -32400
# Node ID 2eafa89733ed584d7c8959d2b8cfb107066be23f
# Parent  f0fa9a755513c5a32dc9df7b46d30823b91bef04
ord-Ord causes od→ord x o< od→ord y → y ∋ x,
it makes y ∋ φ
  dead end

diff -r f0fa9a755513 -r 2eafa89733ed HOD.agda
--- a/HOD.agda	Mon Jul 08 18:19:56 2019 +0900
+++ b/HOD.agda	Mon Jul 08 18:26:33 2019 +0900
@@ -102,6 +102,9 @@
 o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x 
 o<→c< {n} {x} {y} lt = subst ( λ k → k o< y ) ord-Ord lt 
 
+o<→c<'  : {n : Level} {x y : OD {suc n} } → od→ord x o< od→ord y → y ∋ x 
+o<→c<' {n} {x} {y} lt = def-subst {suc n} {Ord (od→ord y)} {od→ord x} {y} {od→ord x} lt Ord-ord-≡ refl
+
 sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )