--- a/FL.agda	Sat Sep 12 09:26:39 2020 +0900
+++ b/FL.agda	Sat Sep 12 22:18:30 2020 +0900
@@ -176,16 +176,24 @@
 FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
 ... | [] | ()
 ... | cons a₁ t x₂ | e = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
-FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLinsert x  (cons a₁ y x₂)
+FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 a<x) with total x a₁
+... | inj₁ (case1 refl) =  cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
+... | inj₂ (case1 refl) =  cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
+... | inj₁ (case2 x<a₁) =  cons a (cons x  (cons a₁ y x₂) ( Level.lift (fromWitness x<a₁) , ttf x<a₁ y x₂))
+                   (  Level.lift (fromWitness a<x) , ttf a<x (cons  a₁ y x₂) ( Level.lift (fromWitness x<a₁) , ttf x<a₁ y x₂))
+... | inj₂ (case2 a₁<x) with FLinsert x y
 ... | [] = []
-... | cons a₂ t x₁ with total a₁ a₂
-... | inj₁ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
-... | inj₁ (case2 lt2)  = cons a (cons a₂ t x₁) ( Level.lift (fromWitness a<a₂) , ttf a<a₂ t  x₁) where
-     a<a₂ : a f< a₂
-     a<a₂ = f<-trans (toWitness a<a₁) lt2
-... | inj₂ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
-... | inj₂ (case2 lt2)  = cons a (cons a₂ t x₁)  ( Level.lift (fromWitness a<a₂) , ttf a<a₂ t  x₁) where
-     a<a₂ : a f< a₂   -- lt : a f< x
-     a<a₂  = {!!}
+... | cons a₂ t x₁ = cons a ( cons a₁ ( cons a₂ t x₁ ) ( Level.lift (fromWitness ttf0) , ttf ttf0 t x₁))
+               ( Level.lift a<a₁ ,  Level.lift (fromWitness ttf1) , ttf ttf1 t x₁ ) where
+    ttf0 : a₁ f< a₂
+    ttf0 = ?
+    ttf1 : a  f< a₂
+    ttf1 = f<-trans (toWitness a<a₁) ttf0 
+
+
+-- a₁<x  : a₁ f< x
+-- a<x   : a f< x
+-- a<a₁  : T (isYes (a f<? a₁ | FLcmp a a₁))
+
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1