new intro:

[helm.git] / helm / software / matita / nlibrary / re / re.ma

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index f8916ee5a5759682c9808c1c4238444780cadbe7..300812ce89ccff39d7be66f2b507ad6097496684 100644 (file)
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -65,14 +65,7 @@ nqed. *)
 
 nlemma in_l_inv_e:
  ∀S,w. in_l S w (e ?) → w = [].
- #S; #w; #H; ninversion H
-  [ #a; #b; ndestruct; //
-  | #a; #b; #c; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; ndestruct
-  | #a; #b; #c; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
+ #S; #w; #H; ninversion H; #; ndestruct; //.
 nqed.
 
 naxiom in_l_inv_s: 
@@ -141,7 +134,7 @@ ntheorem eclose_true:
   true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
  #S; #E; nelim E; nnormalize; //
   [ #H; ncases (?: False); /2/
-  | #x; #H; ncases (?: False); /2/
+  | #x H; #H; ncases (?: False); /2/
   | #x; #H; ncases (?: False); /2/
   | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
     #_; #_; #H; ncases (?:False); /2/
@@ -165,15 +158,10 @@ nqed.
 ntheorem in_l_empty_c:
  ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
  #S; #E1; #E2; #H; ninversion H
-  [ #_; #H2; ndestruct
-  | #x; #K; ndestruct
+  [##1,2,4,5,6,7: #; ndestruct
   | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
     nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
-    ndestruct; //
-  | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
-  | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
-  | #E; #_; #K; ndestruct 
-  | #w1; #w2; #w3; #H1; #H2; #H3; #H4; #H5; #H6; ndestruct ]
+    ndestruct; // ]
 nqed.
 
 ntheorem eclose_true':
@@ -185,25 +173,15 @@ ntheorem eclose_true':
   | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
      [ #H1; #H2; #H3; ninversion H3; /3/;
    ##| #H1; #H2; #H3; ninversion H3
-        [ #_; #K; ndestruct
-        | #x; #K; ndestruct
+        [ ##1,2,4,5,6,7: #; ndestruct
         | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
-          napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //
-        | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
-        | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
-        | #E'; #_; #K; ndestruct
-        | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]##]
+          napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##]
 ##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
     #E2; #H1; #H2; #H3; ninversion H3
-     [ #_; #K; ndestruct
-     | #w; #_; #K; ndestruct
-     | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
+     [ ##1,2,3,5,6,7: #; ndestruct; /2/
      | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
        ncases (?: False); napply (absurd ?? (not_eq_true_false …));
-       /2/
-     | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/
-     | #a; #b; #c; ndestruct
-     | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##]
+       /2/ ]##]
 nqed.     
 
 (*