From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 19 Jul 2010 09:29:50 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2876
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39401f3f920f7117d458e92b8113eae47205d6a5;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 7b6580c87..36abab4f6 100644
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -489,6 +489,19 @@ nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 .|\fst e|)^
     nrewrite < (cup0 ? (𝐋\p e')); //;##]
 nqed.
 
+(* corollary 17: non tipa *)
+
+nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w.
+#S f g H; nrewrite > H; //; nqed.
+ 
+(* corollary 18 *)
+ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ .|e|.
+#S e; @;
+##[ #defsnde; nlapply (bull_cup ? e); nchange in match (𝐋\p (•e)) with (?∪?);
+    nrewrite > defsnde; #H; 
+    nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //;
+    E MO?
+
 STOP
 
 notation > "\move term 90 x term 90 E"