# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599957237 -32400
# Node ID 5e5e6cd7da2ea107a33cec541f908a9e3504af94
# Parent  c5ed0175ecb9febc3d45042a191c03851f24aafa
FLinsert done

diff -r c5ed0175ecb9 -r 5e5e6cd7da2e FL.agda
--- a/FL.agda	Sun Sep 13 04:27:17 2020 +0900
+++ b/FL.agda	Sun Sep 13 09:33:57 2020 +0900
@@ -149,15 +149,17 @@
 FLinsert {suc n} x (cons a y yr) |  tri> ¬a ¬b a<x =
         cons a (FLinsert x y) (FLfresh a x y a<x yr )
 
-FLfresh {n} a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
-FLfresh {n} a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
+FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
+FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x)  , Level.lift a<b , Level.lift tt
 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
 ... | tri> ¬a ¬b b<x = Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
-FLfresh {n} a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) with FLcmp x b
-... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , {!!} , {!!} , ttf {!!} y x₁ 
-... | tri≈ ¬a refl ¬c =  Level.lift (fromWitness a<x)  , {!!} , ttf {!!}  y x₁
-... | tri> ¬a ¬b b<x = {!!} , {!!} 
-
+FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
+... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
+... | tri≈ ¬a refl ¬c =  Level.lift (fromWitness a<x)  , ttf a<x y br
+FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
+    Level.lift a<b ,  Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
+FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
+    Level.lift a<b , FLfresh a x  (cons a₁ y x₁) a<x a<y
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1