previously hidden simplifications (in old destruct) added

diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma
index c9ef72c8ae4989ed600205ea88cf9dd29b5b6fe9..c9cab27f85e542b71265fd2244dfa9c9a1ecdce8 100644 (file)
--- a/helm/software/matita/dama/ordered_groups.ma
+++ b/helm/software/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/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index dede79ca145e741115813aac4ebff05b48cedb13..36217ad9dbfba62e8299b06789df498f38d47456 100644 (file)
--- a/helm/software/matita/tests/coercions_russell.ma
+++ b/helm/software/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 ? ? []);