--- a/agda/regular-concat.agda	Tue Mar 16 14:02:45 2021 +0900
+++ b/agda/regular-concat.agda	Wed Mar 17 10:24:49 2021 +0900
@@ -153,8 +153,8 @@
     abmove (case1 q) h = case1 (δ (automaton A) q h)
     abmove (case2 q) h = case2 (δ (automaton B) q h)
     lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
-    lemma-nmove-ab (case1 q) _ = equal?-refl (afin A)
-    lemma-nmove-ab (case2 q) _ = equal?-refl (afin B)
+    lemma-nmove-ab (case1 q) _ = ? -- equal?-refl (afin A)
+    lemma-nmove-ab (case2 q) _ = ? -- equal?-refl (afin B)
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
        exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
     nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
@@ -180,7 +180,7 @@
     acceptAB : Split (contain A) (contain B) x
         → Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
     acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
-        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
+        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) ? (prop0 S) (prop1 S) )
 
     closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
     closed-in-concat→ concat with split→AB (contain A) (contain B) x concat