--- a/LEMC.agda	Sun Jul 05 15:49:00 2020 +0900
+++ b/LEMC.agda	Sun Jul 05 16:56:21 2020 +0900
@@ -112,7 +112,7 @@
                  lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
                  lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
               np : ¬ (p =h= od∅)
-              np p∅ =  NP (λ y p∋y → ∅< p∋y p∅ ) 
+              np p∅ =  NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) 
               y1choice : choiced p
               y1choice = choice-func p np
               y1 : HOD
@@ -126,9 +126,9 @@
          cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced x 
          cx {x} nx = choice-func x nx
          minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
-         minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 
+         minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) 
          x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) 
+         x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) 
          minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
          minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y