From a97797680ffd7f1cc96803e25f4879211e1e6d66 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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