# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559076365 -32400
# Node ID d13d1351a1face0834e5e81a71215ae58a7807df
# Parent  323b561210b538074bf69b753a353831f07b4fda
                 lemma = cong₂ (λ x not → minimul x not ) oiso { }6
Cannot instantiate the metavariable _1342 to solution (x == od∅ →
⊥) since it contains the variable x which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution

diff -r 323b561210b5 -r d13d1351a1fa ordinal-definable.agda
--- a/ordinal-definable.agda	Tue May 28 23:02:50 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 05:46:05 2019 +0900
@@ -260,6 +260,8 @@
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7  eq )
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -368,13 +370,15 @@
             reg1 :  Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
             reg1 = record { eq→ = reg0  ; eq← = λ () } where
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
-         ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  where
+         ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
-         proj1 (regularity x not ) = minimul<x x not
-         proj2 (regularity x not ) = record { eq→ = reg4 ; eq← = λ () } where
-            reg4 :  {xd : Ordinal } → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) xd → def od∅ xd
-            reg4 {xd} = {!!} (eq→ (proj1 (regularity-ord {!!} {!!} )) )
+         regularity x not =  
+             subst₂ ( λ x min  → (x ∋ min) ∧ (Select min (λ x₁ → (min ∋ x₁) ∧ (x ∋ x₁)) == od∅) )
+                              oiso lemma ( regularity-ord (od→ord x) (subst (λ k → ¬ (k == od∅) ) (sym oiso) not )) where
+                 lemma : minimul (ord→od (od→ord x)) (subst (λ k → ¬ (k == od∅)) (sym oiso) not) ≡ minimul x not
+                 lemma = cong₂ (λ x not → minimul x not ) oiso {!!}
+