wip ....

[helm.git] / matita / matita / lib / tutorial / chapter8.ma

diff --git a/matita/matita/lib/tutorial/chapter8.ma b/matita/matita/lib/tutorial/chapter8.ma
index b9bc64a9c79467212b8efeef2eb668ba8e77d940..47cfbdeb7b392e6539c1ff877898334142e64fe4 100644 (file)
--- a/matita/matita/lib/tutorial/chapter8.ma
+++ b/matita/matita/lib/tutorial/chapter8.ma
@@ -5,6 +5,7 @@ We shall apply all the previous machinery to the study of regular languages
 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: *)
@@ -270,8 +271,8 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w.
 (* Below are a few, simple, semantic properties of items. In particular:
 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
 The first property is proved by a simple induction on $i$; the other
 results are easy corollaries. We need an auxiliary lemma first. *)