# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561976023 -32400
# Node ID 69a845b82854fb5cee4dd5ecd432d47e0721ba83
# Parent  870fe02c7a076763f9f7ccb2cf3b4400502767c2
...  dead end?

diff -r 870fe02c7a07 -r 69a845b82854 HOD.agda
--- a/HOD.agda	Mon Jul 01 16:03:15 2019 +0900
+++ b/HOD.agda	Mon Jul 01 19:13:43 2019 +0900
@@ -343,7 +343,7 @@
          --
          --  if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
-         --    In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
+         --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
          --
          POrd : {A t : HOD} → Power A ∋ t → Power A ∋ Ord (od→ord t)
          POrd {A} {t} P∋t = o<→c< P∋t
@@ -359,7 +359,7 @@
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
-              lemma1 lt = ?
+              lemma1 lt = {!!}
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t