--- a/FL.agda	Tue Sep 08 11:07:27 2020 +0900
+++ b/FL.agda	Tue Sep 08 12:29:58 2020 +0900
@@ -117,7 +117,13 @@
 
 total : {n : ℕ } → Total (_f≤_ {n})
 total f0 f0 = inj₁  (case1 refl) 
-total (x :: xt) (y :: yt) = {!!}
+total (x :: xt) (y :: yt) with <-fcmp x y
+... | tri< a ¬b ¬c = inj₁ (case2 (f<n a))
+... | tri> ¬a ¬b c = inj₂ (case2 (f<n c))
+... | tri≈ ¬a b ¬c with FLcmp xt yt
+... | tri< a ¬b ¬c₁ = inj₁ (case2 (subst (λ k → (x :: xt ) f< (k :: yt) ) b (f<t a)))
+... | 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 Data.List.Fresh
@@ -140,22 +146,32 @@
 -- open import Data.Maybe
 -- open TotalOrder
 
+open import Relation.Nullary.Decidable hiding (⌊_⌋)
+open import Data.Bool -- hiding (T)
+open import Data.Unit.Base using (⊤ ; tt)
+
+-- T : Data.Bool.Bool → Set
+-- T true  = ⊤
+-- T false = ⊥
+
+
 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 FLcmp x a
-... | tri≈ ¬a b ¬c = (cons a y x₁)
-... | tri< a₁ ¬b ¬c = cons x ( cons a y x₁) (FLcons1  x₁) where
-   FLcons1 :  a # y →  x # (cons a y x₁)
-   FLcons1 ay with total a x
-   ... | inj₁ (case1 eq) = ⊥-elim ( ¬b (sym eq) )
-   ... | inj₁ (case2 lt) = fromWitness _ (yes lt) , ? 
-   ... | inj₂ (case1 eq) = ⊥-elim ( ¬b eq )
-   ... | inj₂ (case2 lt) = {!!}
-... | tri> ¬a ¬b c with FLcons x y
-... | [] = a ∷# []
-... | cons a₁ t x₂ = cons a ( cons a₁ t x₂ ) FLcons2 where
-   FLcons2 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a  (cons a₁ t x₂)
-   FLcons2 =  {!!} , {!!}
+FLcons {suc n} x (cons a y x₁) with total x a
+... | inj₁ (case1 eq) = cons a y x₁
+... | inj₁ (case2 lt) = cons x (cons a y x₁) ( Level.lift ttt , ttf ) where
+   tty :  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y
+   tty = x₁
+   ttf :  fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
+   ttf = {!!}
+   tt1 : true ≡ isYes (x f<? a)
+   tt1 with x f<? a
+   ... | yes y = refl
+   ... | no n = ⊥-elim ( n lt )
+   ttt :  T (isYes (x f<? a ))
+   ttt = subst (λ k → Data.Bool.T k ) tt1 tt
+... | inj₂ (case1 eq) = cons a y x₁
+... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}
 
 fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1