+
+notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+interpretation "star" 'pk a = (k ? a).
+interpretation "or" 'plus a b = (o ? a b).
+
+notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+interpretation "cat" 'pc a b = (c ? a b).
+
+(* to get rid of \middot *)
+ncoercion c : ∀S:Alpha.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?.
+
+notation < "a" non associative with precedence 90 for @{ 'ps $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
+interpretation "atom" 'ps a = (s ? a).
+
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (e ?).
+
+notation "∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
+
+nlet rec flatten (S : Alpha) (l : list (word S)) on l : word S ≝
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+
+nlet rec conjunct (S : Alpha) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
+match l with [ nil ⇒ ? | cons w tl ⇒ r w ∧ conjunct ? tl r ]. napply True. nqed.
+
+ndefinition empty_lang ≝ λS.λw:word S.False.
+notation "{}" non associative with precedence 90 for @{'empty_lang}.
+interpretation "empty lang" 'empty_lang = (empty_lang ?).
+
+ndefinition sing_lang ≝ λS.λx,w:word S.x=w.
+notation "{x}" non associative with precedence 90 for @{'sing_lang $x}.
+interpretation "sing lang" 'sing_lang x = (sing_lang ? x).
+
+ndefinition union : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:word S.l1 w ∨ l2 w.
+interpretation "union lang" 'union a b = (union ? a b).
+
+ndefinition cat : ∀S,l1,l2,w.Prop ≝
+ λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+interpretation "cat lang" 'pc a b = (cat ? a b).
+
+ndefinition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
+interpretation "star lang" 'pk l = (star ? l).
+
+notation > "𝐋 term 70 E" non associative with precedence 75 for @{in_l ? $E}.
+nlet rec in_l (S : Alpha) (r : re S) on r : word S → Prop ≝
+match r with
+[ z ⇒ {}
+| e ⇒ { [ ] }
+| s x ⇒ { [x] }
+| c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
+| o r1 r2 ⇒ 𝐋 r1 ∪ 𝐋 r2
+| k r1 ⇒ (𝐋 r1) ^*].
+notation "𝐋 term 70 E" non associative with precedence 75 for @{'in_l $E}.
+interpretation "in_l" 'in_l E = (in_l ? E).
+interpretation "in_l mem" 'mem w l = (in_l ? l w).
+
+notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
+interpretation "orb" 'orb a b = (orb a b).
+
+ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
+notation > "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
+
+ninductive pitem (S: Alpha) : Type[0] ≝
+ pz: pitem S
+ | pe: pitem S
+ | ps: S → pitem S
+ | pp: S → pitem S
+ | pc: pitem S → pitem S → pitem S
+ | po: pitem S → pitem S → pitem S
+ | pk: pitem S → pitem S.
+
+ndefinition pre ≝ λS.pitem S × bool.
+
+interpretation "pstar" 'pk a = (pk ? a).
+interpretation "por" 'plus a b = (po ? a b).
+interpretation "pcat" 'pc a b = (pc ? a b).
+notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "ppatom" 'pp a = (pp ? a).
+(* to get rid of \middot *)
+ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?.
+interpretation "patom" 'ps a = (ps ? a).
+interpretation "pepsilon" 'epsilon = (pe ?).
+interpretation "pempty" 'empty = (pz ?).
+
+notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
+nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
+ match l with
+ [ pz ⇒ ∅
+ | pe ⇒ ϵ
+ | ps x ⇒ `x
+ | pp x ⇒ `x
+ | pc E1 E2 ⇒ (|E1| · |E2|)
+ | po E1 E2 ⇒ (|E1| + |E2|)
+ | pk E ⇒ |E|^* ].
+notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
+interpretation "forget" 'forget a = (forget ? a).
+
+notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
+interpretation "fst" 'fst x = (fst ? ? x).
+notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
+interpretation "snd" 'snd x = (snd ? ? x).
+
+notation > "𝐋\p\ term 70 E" non associative with precedence 75 for @{in_pl ? $E}.
+nlet rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝
+match r with
+[ pz ⇒ {}
+| pe ⇒ {}
+| ps _ ⇒ {}
+| pp x ⇒ { [x] }
+| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 |r2| ∪ 𝐋\p\ r2
+| po r1 r2 ⇒ 𝐋\p\ r1 ∪ 𝐋\p\ r2
+| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (|r1|^* ) ].
+notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'in_pl $E}.
+notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'in_pl $E}.
+interpretation "in_pl" 'in_pl E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+ndefinition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
+
+interpretation "epsilon" 'epsilon = (epsilon ?).
+notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
+interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
+
+ndefinition in_prl ≝ λS : Alpha.λp:pre S. 𝐋\p (\fst p) ∪ ϵ (\snd p).
+
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_pl E = (in_prl ? E).
+
+nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
+#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
+
+(* lemma 12 *)
+nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
+#S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//;
+nnormalize; *; ##[##2:*] nelim e;
+##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
+##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
+##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
+*; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
+nqed.