--- a/FL.agda	Tue Sep 08 17:33:49 2020 +0900
+++ b/FL.agda	Wed Sep 09 10:53:20 2020 +0900
@@ -48,6 +48,12 @@
 ... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt )  refl (λ lt → f-≡< refl lt )
 ... | tri> ¬a₁ ¬b c = tri> (λ lt  → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)
 
+f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
+f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ )
+f<-trans {suc n} (f<n x) (f<t y<z) = f<n x
+f<-trans {suc n} (f<t x<y) (f<n x) = f<n x
+f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z)
+
 infixr 250 _f<?_
 
 _f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
@@ -116,7 +122,7 @@
 ... | tri≈ ¬a₁ b₁ ¬c₁ = inj₁ (case1 (subst₂ (λ j k → j :: k ≡ y :: yt ) (sym b)  (sym b₁ ) refl  ))
 ... | tri> ¬a₁ ¬b c = inj₂ (case2 (subst (λ k → (y :: yt ) f< (k :: xt) ) (sym b) (f<t c)))
 
-open import Relation.Nary using (⌊_⌋; fromWitness)
+open import Relation.Nary using (⌊_⌋)
 open import Data.List.Fresh
 open import Data.List.Fresh.Relation.Unary.All
 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
@@ -145,21 +151,29 @@
 -- T true  = ⊤
 -- T false = ⊥
 
-ttf< :  {n : ℕ } → {x a : FL n } → x f< a  → T (isYes (x f<? a))
-ttf< {n} {x} {a} x<a with x f<? a
-... | yes y = subst (λ k → Data.Bool.T k ) refl tt
-... | no nn = ⊥-elim ( nn x<a )
+--  fresh a []        = ⊤
+--  fresh a (x ∷# xs) = R a x × fresh a xs
+
+-- toWitness
+-- ttf< :  {n : ℕ } → {x a : FL n } → x f< a  → T (isYes (x f<? a))
+-- ttf< {n} {x} {a} x<a with x f<? a
+-- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
+-- ... | no nn = ⊥-elim ( nn x<a )
 
-FLcons : {n : ℕ } → FL n → FList {n}  → FList {n} 
-FLcons {zero} f0 y = f0 ∷# []
-FLcons {suc n} x [] = x ∷# []
-FLcons {suc n} x (cons a y x₁) with total x a
+FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
+FLinsert {zero} f0 y = f0 ∷# []
+FLinsert {suc n} x [] = x ∷# []
+FLinsert {suc n} x (cons a y x₁) with total x a
 ... | inj₁ (case1 eq) = cons a y x₁
-FLcons {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (ttf<  lt ) , ttf a y  x₁) where
-   ttf : (a : FL (suc n)) → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
-   ttf a [] fr = Level.lift tt
-   ttf a (cons a₁ y x1) (lift lt1 , _ ) = (Level.lift (ttf< {!!} )) , ttf a₁ y x1
+FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf a lt y  x₁) where
+   ttf : (a : FL (suc n)) → x f< a → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
+   ttf a _ [] fr = Level.lift tt
+   ttf a lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ (ttf1 lt1 lt) y x1 where 
+       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 {!!}) {!!}
+... | 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 = {!!}
 
-fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 
+fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1