--- a/agda/regular-language.agda	Tue Nov 12 18:54:44 2019 +0900
+++ b/agda/regular-language.agda	Wed Nov 13 07:50:31 2019 +0900
@@ -294,12 +294,12 @@
     contain-A [] nq fn qa cond with found← finab fn | found-q (found← finab fn) | cond | inspect found-q (found← finab fn)
     contain-A [] nq fn qa cond | S | s | state-A nq=t | record { eq = refl }  with  nq=t (found-q S) (bool-∧→tt-0 (found-p S))
     ... | refl  = bool-∧→tt-1 (found-p S)
-    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S))
-    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ | case1 refl =  bool-∧→tt-1 (found-p S)
-    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | case2 accept-B = ⊥-elim ( lemma11 accept-B )  where
+    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S)) | inspect (cond-b (found-q S)) (bool-∧→tt-0 (found-p S))
+    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ | case1 refl | _ =  bool-∧→tt-1 (found-p S)
+    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | case2 accept-B | _ = ⊥-elim ( lemma11 accept-B )  where
         lemma11 :  (  nq (case2 qb ) ≡ true → aend (automaton B) qb ≡ false ) → ⊥
         lemma11  accept-B = ¬-bool ( accept-B (bool-∧→tt-0 (found-p S))) (bool-∧→tt-1 (found-p S ))
-    contain-A [] nq fn qa cond | S | case1 qa' | state-AB cond-b | record { eq = refl }  | case2 accept-B = {!!}
+    contain-A [] nq fn qa cond | S | case1 qa' | state-AB cond-b | record { eq = refl }  | case2 accept-B | record { eq = ee} = {!!}
     contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
     ... | yes eq = bool-or-41 eq
     ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h)  {!!} ) where