+(* We are ready to give the formal definition of the Kleene's star of l:
+a word w belongs to l* is and only if there exists a list of strings
+lw such that (conjunct lw l) and l = flatten lw. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="star"\ 6definition star ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw.\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l.
+notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
+interpretation "star lang" 'star l = (star ? l).
+
+(* The derivative of a language A with respect to a character a is the set of
+all strings w such that aw is in A. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="deriv"\ 6definition deriv ≝ λS.λA:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.λa,w. A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w).
+
+(*
+\ 5h2 class="section"\ 6Language equalities\ 5/h2\ 6
+Equality between languages is just the usual extensional equality between
+sets. The operation of concatenation behaves well with respect to this equality. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="cat_ext_l"\ 6lemma cat_ext_l: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w1) /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="cat_ext_r"\ 6lemma cat_ext_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w2) /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+(* Concatenating a language with the empty language results in the
+empty language. *)
+\ 5img class="anchor" src="icons/tick.png" id="cat_empty_l"\ 6lemma cat_empty_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S→Prop. \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+qed.
+
+(* Concatenating a language l with the singleton language containing the
+empty string, results in the language l; that is {ϵ} is a left and right
+unit with respect to concatenation. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="epsilon_cat_r"\ 6lemma epsilon_cat_r: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+ A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
+ |#inA @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="epsilon_cat_l"\ 6lemma epsilon_cat_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
+ |#inA @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+ qed.
+
+(* Concatenation is distributive w.r.t. union. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="distr_cat_r"\ 6lemma distr_cat_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+ (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C.
+#S #A #B #C #w %
+ [* #w1 * #w2 * * #eqw * /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ |* * #w1 * #w2 * * /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="distr_cat_r_eps"\ 6lemma distr_cat_r_eps: ∀S.∀A,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+ (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C.
+ #S #A #C @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6 |@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"\ 6epsilon_cat_l\ 5/a\ 6]
+qed.
+
+(* The following is a major property of derivatives *)
+
+\ 5img class="anchor" src="icons/tick.png" id="deriv_middot"\ 6lemma deriv_middot: ∀S,A,B,a. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S (A\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6B) a \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (\ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S A a) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
+#S #A #B #a #noteps #w normalize %
+ [* #w1 cases w1
+ [* #w2 * * #_ #Aeps @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
+ #H #H1 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w2) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w3) % // % //
+ ]
+ |* #w1 * #w2 * * #H #H1 #H2 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w1))
+ @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w2) % // % normalize //
+ ]
+qed.
+
+(*
+\ 5h2 class="section"\ 6Main Properties of Kleene's star\ 5/h2\ 6
+We conclude this section with some important properties of Kleene's
+star that will be used in the following chapters. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="espilon_in_star"\ 6lemma espilon_in_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+ A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6.
+#S #A @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/True.con(0,1,0)"\ 6I\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="cat_to_star"\ 6lemma cat_to_star:∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+ ∀w1,w2. A w1 → A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 w2 → A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 (w1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6w2).
+#S #A #w1 #w2 #Aw * #l * #H #H1 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (w1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))
+% normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="fix_star"\ 6lemma fix_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+ A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
+#S #A #w %
+ [* #l generalize in match w; -w cases l [normalize #w * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
+ #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
+ #w1A #cw1 %1 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w1) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 S tl))
+ % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ whd @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … tl) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |* [2: whd in ⊢ (%→?); #eqw <eqw //]
+ * #w1 * #w2 * * #eqw <eqw @\ 5a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"\ 6cat_to_star\ 5/a\ 6
+ ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="star_fix_eps"\ 6lemma star_fix_eps : ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+ A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
+#S #A #w %
+ [* #l elim l
+ [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
+ |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
+ |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1
+ @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w1)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 S tl)) %
+ [% [@H1 | normalize % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] |whd @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … tl) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
+ ]
+ ]
+ |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @\ 5a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"\ 6cat_to_star\ 5/a\ 6 //
+ | whd in ⊢ (%→?); #H <H //
+ ]
+ ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="star_epsilon"\ 6lemma star_epsilon: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+ A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
+#S #A #w % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * //
+qed.
+
\ No newline at end of file