From a97797680ffd7f1cc96803e25f4879211e1e6d66 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 8 Jun 2008 17:12:43 +0000
Subject: [PATCH] Generalize no more required for elim.
---
helm/software/matita/library/list/list.ma | 3 +--
helm/software/matita/library/list/sort.ma | 7 ++-----
2 files changed, 3 insertions(+), 7 deletions(-)
diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index ad44bd63a..f9f39bebf 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -178,8 +178,7 @@ lemma list_ind2 :
(âtl1,tl2,hd1,hd2. P tl1 tl2 â P (hd1::tl1) (hd2::tl2)) â
P l1 l2.
intros (T1 T2 l1 l2 P Hl Pnil Pcons);
-generalize in match Hl; clear Hl; generalize in match l2; clear l2;
-elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
+elim l1 in Hl l2 ⢠% 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl]
intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
qed.
diff --git a/helm/software/matita/library/list/sort.ma b/helm/software/matita/library/list/sort.ma
index 857ab4e86..4c67cb636 100644
--- a/helm/software/matita/library/list/sort.ma
+++ b/helm/software/matita/library/list/sort.ma
@@ -147,9 +147,7 @@ lemma ordered_injective:
elim l
[ simplify; reflexivity;
| simplify;
- generalize in match H1;
- clear H1;
- elim l1;
+ elim l1 in H1 ⢠%;
[ simplify; reflexivity;
| cut ((le a a1 \land ordered A le (a1::l2)) = true);
[ generalize in match Hcut;
@@ -181,8 +179,7 @@ lemma insert_sorted:
clear l; intros; simplify; intros;
[2: rewrite > H1;
[ generalize in match (H ? ? H2); clear H2; intro;
- generalize in match H4; clear H4;
- elim l'; simplify;
+ elim l' in H4 ⢠%; simplify;
[ rewrite > H5;
reflexivity
| elim (le x a); simplify;
--
2.39.2