--- a/src/bijection.agda	Sat Jun 24 07:22:43 2023 +0900
+++ b/src/bijection.agda	Sat Jun 24 08:56:47 2023 +0900
@@ -919,29 +919,54 @@
    gi = record { f = g ; inject = g-inject }
    dec0 : (c : List A ∧ List Bool) → Dec (Is (List A) (List A ∧ List Bool) (λ x → g (f x)) c)
    dec0 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl }
-   dec0 ⟪ h ∷ t , [] ⟫ = ?
-   dec0 ⟪ [] , true ∷ bt ⟫ = ?
-   dec0 ⟪ [] , false ∷ bt ⟫ = ?
+   dec0 ⟪ h ∷ t , [] ⟫ = no ( lem00 ) where
+        lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , [] ⟫ → ⊥
+        lem00 record { a = [] ; fa=c = () }
+        lem00 record { a = (x ∷ a) ; fa=c = () }
+   dec0 ⟪ [] , true ∷ bt ⟫ = no lem00 where
+        lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , true ∷ bt ⟫ → ⊥
+        lem00 record { a = [] ; fa=c = () }
+   dec0 ⟪ [] , false ∷ bt ⟫ = no lem00 where
+        lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , false ∷ bt ⟫ → ⊥
+        lem00 record { a = [] ; fa=c = () }
    dec0 ⟪ h ∷ t , (true ∷ bt) ⟫ with dec0 ⟪ t , bt ⟫
    ... | yes y = yes record { a = h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))  }
-   ... | no n = no ( λ np →  ⊥-elim ( n record { a = ? ; fa=c = ? }  ) )
-   dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no ( λ np → ? )
+   ... | no n = no lem00  where
+        lem00 : ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , true ∷ bt ⟫
+        lem00 record { a = (x ∷ a) ; fa=c = refl } = ⊥-elim ( n record { a = a ; fa=c = refl } )
+   dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no lem00 where
+        lem00 :  ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , false ∷ bt ⟫
+        lem00 record { a = [] ; fa=c = () }
+        lem00 record { a = (x ∷ a) ; fa=c = () }
    dec1 : (c : List A ∧ List Bool) → Dec (Is (List (Maybe A)) (List A ∧ List Bool) g c)
    dec1 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl }
-   dec1 ⟪ h ∷ t , [] ⟫ = ?
-   dec1 ⟪ [] , _ ∷ bt ⟫ = ?
+   dec1 ⟪ h ∷ t , [] ⟫ = no lem00 where
+        lem00 :  ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , [] ⟫
+        lem00 record { a = (just x ∷ a) ; fa=c = () }
+        lem00 record { a = (nothing ∷ a) ; fa=c = () }
+   dec1 ⟪ [] , true ∷ bt ⟫ = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , true ∷ bt ⟫
+        lem00 record { a = (just x ∷ a) ; fa=c = () }
+        lem00 record { a = (nothing ∷ a) ; fa=c = () }
+   dec1 ⟪ [] , false ∷ bt ⟫ with dec1 ⟪ [] , bt ⟫
+   ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) }
+   ... | no n = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , false ∷ bt ⟫
+        lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where
+            lem01 : proj2 (g a) ≡ bt
+            lem01 with cong proj2 eq
+            ... | refl = refl
    dec1 ⟪ h ∷ t , true ∷ bt ⟫ with dec1 ⟪ t , bt ⟫
    ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))   }
-   ... | no n = ?
-   dec1 ⟪ h ∷ t , false ∷ bt ⟫  with dec1 ⟪ t , bt ⟫
-   ... | yes y = yes record { a = nothing ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , false ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))   }
-   ... | no n = ?
+   ... | no n = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , true ∷ bt ⟫
+        lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } 
+   dec1 ⟪ h ∷ t , false ∷ bt ⟫  with dec1 ⟪ h ∷ t , bt ⟫
+   ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) }
+   ... | no n = no lem00 where
+        lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , false ∷ bt ⟫
+        lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where
+            lem01 : proj2 (g a) ≡ bt
+            lem01 with cong proj2 eq
+            ... | refl = refl
 
--- open import Data.Fin
---
---- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n)))
---
---- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n))
---- LBFin = ?
-
---