-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 ≝
+definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6.
+
+interpretation "pstar" 'kstar a = (pstar ? a).
+interpretation "por" 'plus a b = (por ? a b).
+interpretation "pcat" 'concat a b = (pconcat ? a b).
+
+notation "• a" non associative with precedence 90 for @{ 'ppoint $a}.
+(* notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}. *)
+
+interpretation "ppatom" 'ppoint a = (ppoint ? a).
+(* to get rid of \middot
+ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?. *)
+interpretation "patom" 'pchar a = (pchar ? a).
+interpretation "pepsilon" 'epsilon = (pepsilon ?).
+interpretation "pempty" 'empty = (pzero ?).
+
+notation "\boxv term 19 e \boxv" (* slash boxv *) non associative with precedence 70 for @{forget ? $e}.
+
+let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on l: \ 5a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S ≝