# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599938837 -32400
# Node ID c5ed0175ecb9febc3d45042a191c03851f24aafa
# Parent  1db02863ec58373c8bfa6f38571ba2dde491ee27
...

diff -r 1db02863ec58 -r c5ed0175ecb9 FL.agda
--- a/FL.agda	Sun Sep 13 03:38:17 2020 +0900
+++ b/FL.agda	Sun Sep 13 04:27:17 2020 +0900
@@ -150,12 +150,14 @@
         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 y br) a<x (lift a<b , a<y) with FLinsert x (cons b y br)
-... | [] = Level.lift tt
-... | cons i t ir with FLcmp i x
-... | tri< i<x ¬b ¬c = {!!} , {!!}
-... | tri≈ ¬a refl ¬c =  Level.lift (fromWitness a<x) , ttf a<x t ir 
-... | tri> ¬a ¬b x<i =  Level.lift (fromWitness  (f<-trans a<x x<i)) , ttf (f<-trans a<x x<i) t ir
+FLfresh {n} 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 = {!!} , {!!} 
 
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1