--- a/FL.agda	Wed Sep 09 10:53:20 2020 +0900
+++ b/FL.agda	Wed Sep 09 11:14:36 2020 +0900
@@ -172,8 +172,12 @@
        ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
        ttf1 t x<a = f<-trans x<a (toWitness t)
 ... | inj₂ (case1 eq) = cons a y x₁
-... | inj₂ (case2 lt) = cons a (cons x y (ttf2 a lt y x₁)) (Level.lift (fromWitness lt ) , x₁) where
-   ttf2 :  (a : FL (suc n)) → a f< x → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y 
-   ttf2 = {!!}
+... | inj₂ (case2 lt) = cons a ( FLinsert x y ) (ttf2 y) where
+   ttf2 : (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a  (FLinsert x y)
+   ttf2 [] with FLinsert x []
+   ... | [] = Level.lift tt
+   ... | cons a t x = {!!} , {!!}
+   ttf2 (cons a [] x) = {!!}
+   ttf2 (cons a (cons a₁ y x₁) x) = {!!}
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1