X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Flang.ma;h=17269392499df454725ef7597ff781d175534d72;hb=7e6643f9ce7ae87e9241aeac5b6d828e9d47fb63;hp=c1b894a7d787edc592a5f6d29622a4acd104a6ad;hpb=4ed35234de6912d85cb216d61fb523e50449be0b;p=helm.git

diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index c1b894a7d..172693924 100644
--- a/matita/matita/lib/re/lang.ma
+++ b/matita/matita/lib/re/lang.ma
@@ -53,6 +53,10 @@ lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
 cases (H w2) /6/ 
 qed.
   
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+qed.
+
 lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
   (A ∪ B) · C =1  A · C ∪ B · C. 
 #S #A #B #C #w %