X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fcoercions_russell.ma;h=36217ad9dbfba62e8299b06789df498f38d47456;hb=947ee89dec9e60561dfac3ce7e1842f35f178cb8;hp=dede79ca145e741115813aac4ebff05b48cedb13;hpb=48b5f69a87f0f4e067c89085ddd1ae503e53e068;p=helm.git

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index dede79ca1..36217ad9d 100644
--- 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 ? ? []);