the support for reducibility candidates evolves ,,,,

[helm.git] / matita / matita / lib / re / lang.ma

diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index c1b894a7d787edc592a5f6d29622a4acd104a6ad..17269392499df454725ef7597ff781d175534d72 100644 (file)
--- 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 %