-include "basics/list.ma".
-include "basics/sets.ma".
-include "basics/deqsets.ma".
+include "tutorial/chapter5.ma".
definition word ≝ λS:DeqSet.list S.
(A ∪ {ϵ}) · C =1 A · C ∪ C.
#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
qed.
-