--- a/ordinal.agda	Sat May 25 04:58:38 2019 +0900
+++ b/ordinal.agda	Sat May 25 09:09:40 2019 +0900
@@ -60,6 +60,12 @@
       lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
 ordinal-cong refl refl = refl
 
+ordinal-lv : {n : Level} {x y : Ordinal {n}}  → x ≡ y → lv x  ≡ lv y 
+ordinal-lv refl = refl
+
+ordinal-d : {n : Level} {x y : Ordinal {n}}  → x ≡ y → ord x  ≅ ord y 
+ordinal-d refl = refl
+
 ≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t