and the constructions of the associated finite automata. *)
include "tutorial/chapter7.ma".
+include "basics/core_notation/card_1.ma".
(* The type re of regular expressions over an alphabet $S$ is the smallest
collection of objects generated by the following constructors: *)