theory Test

  use seq.Seq
  clone regexp.Regexp with type char = int

  lemma empty_is_empty: forall w: word. not (mem w Empty)

  constant a: int = 0
  constant b: int = 1
  constant c: int = 2

  goal G: mem (cons a (cons b empty)) (Concat (Char a) (Star (Char b)))

end

