--- a/agda/regular-language.agda	Sun Nov 17 12:02:17 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 17 17:47:59 2019 +0900
@@ -284,15 +284,15 @@
 
     ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
     ab-case (case1 qa') qa x = qa'  ≡ qa
-    ab-case (case2 qb) qa x = ¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true )
+    ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x  ≡ true )
 
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
           → (qa : states A )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
     contain-A [] nq fn qa cond with found← finab fn 
     ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
-    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (found (afin B) qb (bool-∧→tt-1 (found-p S)) )) 
     ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
+    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
     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) lemma11 ) where
@@ -304,19 +304,16 @@
        ... | ()   -- δnfa (case2 q) i (case1 q₁) is false
        lemma11 (case2 qb)  ex with found← finab ex 
        ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
-       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb with equal→refl (afin B) (bool-∧→tt-1 (found-p S))
-       ... | refl = contra-position {!!}  ne where
-           lemma14 : exists1 (afin B) (aℕ B) (lt0 (afin B) (aℕ B)) (λ qb → accept (automaton B) qb t) ≡ true →
-                    aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
-           lemma14 = ?
-           lemma12 : exists1 (afin B) (aℕ B) (lt0 (afin B) (aℕ B)) (λ qb → accept (automaton B) qb t) ≡ true → ⊥
-           lemma12 = {!!}
-           lemma13 : aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true → ⊥
-           lemma13 = ne
-       lemma11 (case2 qb)  ex | S | case1 qa' | record { eq = refl } | nb with bool-∧→tt-1 (found-p S)
-       ... | eee = contra-position  {!!} ne where
-           lemma15 : aend (automaton A) qa' /\ (equal? (afin B) qb (δ (automaton B) (astart B) h)) ≡ true
-           lemma15 = eee
+       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb =
+               contra-position (λ fb → subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb ) nb where
+           lemma13 : accept (automaton B) qb' (h ∷ t) ≡ true → ⊥
+           lemma13 = nb
+           lemma14 : nq (case2 qb') /\ equal? (afin B) (δ (automaton B) qb' h) qb ≡ true
+           lemma14 = found-p S
+       lemma11 (case2 qb)  ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
+       ... | eee = contra-position lemma12 ne where
+           lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
+           lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
     lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where