From: Ferruccio Guidi Date: Tue, 13 Nov 2007 10:35:09 +0000 (+0000) Subject: previously hidden simplifications (in old destruct) added X-Git-Tag: 0.4.95@7852~12 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae98f5490e20dd26ece5804d9847acfba0e4d16b;p=helm.git previously hidden simplifications (in old destruct) added --- diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma index c9ef72c8a..c9cab27f8 100644 --- a/matita/dama/ordered_groups.ma +++ b/matita/dama/ordered_groups.ma @@ -65,9 +65,9 @@ lemma le_zero_x_to_le_opp_x_zero: intros (G x Px); generalize in match (og_ordered_abelian_group_properties ? ? ? (-x) Px); intro; (* ma cazzo, qui bisogna rifare anche i gruppi con ≈ ? *) - rewrite > zero_neutral in H1; - rewrite > plus_comm in H1; - rewrite > opp_inverse in H1; + rewrite > zero_neutral in H; + rewrite > plus_comm in H; + rewrite > opp_inverse in H; assumption. qed. diff --git a/matita/tests/coercions_russell.ma b/matita/tests/coercions_russell.ma index dede79ca1..36217ad9d 100644 --- a/matita/tests/coercions_russell.ma +++ b/matita/tests/coercions_russell.ma @@ -93,7 +93,7 @@ definition find_spec ≝ ∃l1,l2,l3.l = l1 @ [x] @ l2 @ [y] @ l3]. lemma mem_x_to_ex_l1_l2 : ∀l,x.mem ? eqb x l = true → ∃l1,l2.l = l1 @ [x] @ l2. -intros 2; elim l (H hd tl IH H); [destruct H] +intros 2; elim l (H hd tl IH H); [simplify in H; destruct H] generalize in match H; clear H; simplify; apply (eqb_elim x hd); simplify; intros; [1:clear IH; rewrite < H; apply (ex_intro ? ? []);