--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jan 03 00:55:06 2022 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jan 03 11:41:58 2022 +0900
@@ -494,6 +494,10 @@
 ... | true = true
 ... | false = memberQ finq q qs
 
+--
+-- there is a duplicate element in finite list
+--
+
 phase2 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
 phase2 finq q [] = false
 phase2 finq q (x ∷ qs) with equal? finq q x
@@ -508,6 +512,11 @@
 dup-in-list : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
 dup-in-list {Q} finq q qs = phase1 finq q qs 
 
+--
+-- if length of the list is longer than kinds of a finite set, there is a duplicate
+-- prove this based on the theorem on Data.Fin
+--
+
 dup-in-list+fin : { Q : Set }  (finq : FiniteSet Q) 
    → (q : Q) (qs : List Q )
    → fin-dup-in-list (F←Q  finq q) (map (F←Q finq) qs) ≡ true