--- a/src/OD.agda	Fri Apr 29 15:52:11 2022 +0900
+++ b/src/OD.agda	Fri Apr 29 17:53:31 2022 +0900
@@ -186,6 +186,12 @@
 o≡→== : { x y : Ordinal  } → x ≡  y →  od (* x) == od (* y)
 o≡→==  {x} {.x} refl = ==-refl
 
+*≡*→≡ : { x y : Ordinal  } → * x ≡ * y →  x ≡ y
+*≡*→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) eq )
+
+&≡&→≡ : { x y : HOD  } → & x ≡  & y →  x ≡ y
+&≡&→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) eq )
+
 o∅≡od∅ : * (o∅ ) ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
      lemma0 :  {x : Ordinal} → odef (* o∅) x → odef od∅ x