From 39401f3f920f7117d458e92b8113eae47205d6a5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 Jul 2010 09:29:50 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/re/re.ma | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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" -- 2.39.2