...

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 7b6580c8789b4173cf47f276e447be188a6e0922..36abab4f6ebf54c9673be674703a58793ce69ca3 100644 (file)
--- 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"