(**************************************************************************)
include "re/lang.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: *)