# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599870399 -32400
# Node ID 173b0541c766be85375f44b55918ad0362045887
# Parent  0d59dcbbd0e144a006428dd646509d007f6c7317
...

diff -r 0d59dcbbd0e1 -r 173b0541c766 FL.agda
--- a/FL.agda	Fri Sep 11 12:26:22 2020 +0900
+++ b/FL.agda	Sat Sep 12 09:26:39 2020 +0900
@@ -184,12 +184,8 @@
      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 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₂
-    ttf3 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ y x₂)
-    ttf3 = 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₂  = {!!}
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1