+(* 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.