--- a/automaton-in-agda/src/derive.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -5,6 +5,7 @@
 open import Data.List hiding ( [_] )
 open import Data.Empty 
 open import finiteSet
+open import finiteFunc
 open import fin
 
 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
@@ -74,7 +75,7 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 -- open import nfa
-open import Data.Nat
+open import Data.Nat hiding (eq?)
 open import Data.Nat.Properties hiding ( eq? )
 open import nat
 open import finiteSetUtil
@@ -261,10 +262,10 @@
    sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? ) 
         ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? )
         ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? ))
-   sb01 isb with ISB.is-sub isb | inspect ISB.is-sub isb 
-   ... | sub&1 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case1 refl
-   ... | sub&2 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case2 (case1 refl)
-   ... | sub&& .r .r₁ z x t | record { eq = refl } = case2 (case2 refl)
+   sb01 isb with ISB.is-sub isb in eq
+   ... | sub&1 .r .r₁ .(ISB.s isb) t = case1 ?
+   ... | sub&2 .r .r₁ .(ISB.s isb) t = case2 (case1 ?)
+   ... | sub&& .r .r₁ z x t = case2 (case2 ?)
    sb00 : ISB r → Bool
    sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub }
 sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? }