X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Flang.ma;h=378a3a76298b9422ab4c8cfa04c88023068ef9e8;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=7424522c7fcb00a784431ca666e85e8c8f44e2f0;hpb=bc477154d15f6979c948f9af602199af547d193e;p=helm.git

diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index 7424522c7..378a3a762 100644
--- a/matita/matita/lib/re/lang.ma
+++ b/matita/matita/lib/re/lang.ma
@@ -30,11 +30,8 @@ definition cat : ∀S,l1,l2,w.Prop ≝
 notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
 
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-
 let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ ⊤ | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
+match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
 
 (* kleene's star *)
 definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
@@ -89,7 +86,7 @@ qed.
 lemma cat_to_star:∀S.∀A:word S → Prop.
   ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
 #S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) 
-% normalize /2/
+% normalize destruct /2/
 qed.
 
 lemma fix_star: ∀S.∀A:word S → Prop. 
@@ -98,7 +95,7 @@ lemma fix_star: ∀S.∀A:word S → Prop.
   [* #l generalize in match w; -w cases l [normalize #w * /2/]
    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
    #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
-   % /2/ whd @(ex_intro … tl) /2/
+   % destruct /2/ whd @(ex_intro … tl) /2/
   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
    * #w1 * #w2 * * #eqw <eqw @cat_to_star 
   ]