From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 14:08:51 +0000 (+0000) Subject: generalize no more useful for elim X-Git-Tag: make_still_working~5061 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc8cd675d2a0635463e7a5399a17dcbd1360c284;p=helm.git generalize no more useful for elim --- diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma index dff89f8d3..9c2f8890b 100644 --- a/helm/software/matita/library/decidable_kit/decidable.ma +++ b/helm/software/matita/library/decidable_kit/decidable.ma @@ -170,7 +170,7 @@ intros (m n); apply bool_to_eq; split; [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption] rewrite > (eqb_true_to_eq ? ? H1); simplify; rewrite > leb_refl; reflexivity -|2: generalize in match m; clear m; elim n 0; +|2: elim n in m ⊢ % 0; [1: simplify; intros; cases n1; reflexivity; |2: intros 1 (m); elim m 0; [1: intros; apply (p2bT ? ? (orbP ? ?)); diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index a38d5eb83..a7db00c72 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/matita/library/decidable_kit/list_aux.ma @@ -58,8 +58,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ] apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity] simplify; intros (tl1 tl2 hd1 hd2 IH H); cases (b2pT ? ? (andbP ? ?) H); rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity -| generalize in match H; clear H; generalize in match l2; clear l2; - elim l1 1 (l1 x1); +| elim l1 in H l2 ⊢ % 1 (l1 x1); [ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;] | intros 3 (tl1 IH l2); cases l2; [ unfold Not; intros; destruct H1;