automaton theory を Gears 形式 ( {t : Set} → f I ( O → t ) → t で書く
automaton の証明手法をGearsで使えるようになる。