# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1491746330 -32400
# Node ID 9902722e157893cd3a568c8d56df46b2771d6050
# Parent  6277ac99db37467aa0ebdecb3b591c9d7157703e
close

diff -r 6277ac99db37 -r 9902722e1578 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Sun Apr 09 22:56:26 2017 +0900
+++ b/SetsCompleteness.agda	Sun Apr 09 22:58:50 2017 +0900
@@ -242,7 +242,14 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; snequ =   λ {i} {j} f → elem (TMap t i x) (comm2 t f )  }
-             ≡⟨ ? ⟩
+             ≡⟨ ≡cong2 ( λ x y →   record { snmap = λ i → x i  ; snequ = λ {i} {j} f → y x i j f }   ) 
+                 ( extensionality Sets  ( λ  i →   eq1  x i ) )
+                   ( extensionality Sets  ( λ  x'  → 
+                   ( extensionality Sets  ( λ  i  → 
+                     ( extensionality Sets  ( λ  j  → 
+                       ( extensionality Sets  ( λ  f'  → elm-cong (elem (x' i ) {!!} ) {!!}  (   eq1  x i   )
+                     ))))))))
+              ⟩ 
                   record {  snmap = λ i →  snmap  (f x ) i  ; snequ =  snequ (f x)  }
              ≡⟨⟩
                   f x