# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574574740 -32400
# Node ID 14cf0e1c8d91b952118bc258af91b8a972ae07e1
# Parent  65bea0aad36361084b8c53f179035f0e91d95ece
...

diff -r 65bea0aad363 -r 14cf0e1c8d91 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 24 14:30:11 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 14:52:20 2019 +0900
@@ -425,10 +425,10 @@
    ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
    ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
    ISO.iso→ iso x with ISO.A←B iso x  
-   ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n | inspect (λ x → ISO.B←A iso ( ISO.A←B iso x )) x
-   ... | tri> ¬a ¬b c | record { eq = e } = ⊥-elim ( nat-≤> c (elm<n x) )
-   ... | tri< a ¬b ¬c | record { eq = e } = {!!}
-   ... | tri≈ ¬a b ¬c | record { eq = e } = begin
+   ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n 
+   ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c (elm<n x) )
+   ... | tri< a ¬b ¬c =  {!!}
+   ... | tri≈ ¬a b ¬c =  begin
            record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = lemma5 }
        ≡⟨ Fin-<-cong (s≤s n<m) fa _ _ (sym (lemma2 b)) lemma7 ⟩
            record { elm = elm x ; elm<n = elm<n x }