--- a/FL.agda	Fri Sep 11 10:55:06 2020 +0900
+++ b/FL.agda	Fri Sep 11 12:26:22 2020 +0900
@@ -166,11 +166,6 @@
        ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
        ttf1 t x<a = f<-trans x<a (toWitness t)
 
-FLmin : {n : ℕ } → FList {n}  → FL n
-FLmin {zero} [] = {!!}
-FLmin {zero} (cons a x x₁) = {!!}
-FLmin {suc n} x = {!!}
-
 FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
 FLinsert {zero} f0 y = f0 ∷# []
 FLinsert {suc n} x [] = x ∷# []
@@ -190,8 +185,10 @@
      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 x (cons a₁ y x₂) ttf2) ( Level.lift (fromWitness lt) , ttf3 ) where
+    x<a₂ : x f< a₂
+    x<a₂ = ?
     ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ x (cons a₁ y x₂) --  a f< x ,  a₂ f< a₁, a < a₁ → x < a₁ , x f< a₂
-    ttf2 = {!!} ,  ttf (f<-trans {!!} lt2 ) y  x₂
+    ttf2 = {!!} ,  ttf (f<-trans {!!} lt2 ) y x₂
     ttf3 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ y x₂)
     ttf3 = Level.lift a<a₁ , fr-ay