val faToDFA = nfaToDFA o efaToNFA o faToEFA;

fun subst(fa, x, y) =
      if FA.accepted fa x
      then FA.union
           (injDFAToFA (DFA.minus(faToDFA fa, faToDFA(strToFA x))),
            strToFA y)
      else fa;