X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Fin.ma;h=0e3be3a8f221ffd21a2809ad0cf43518f49af3e5;hb=92ff0c811f55b37004e2ee45dff0859c31857128;hp=cd372394bfcca4a3de87c1498648137a220b5d2c;hpb=bfb7fbf61e86114e49cb3671503e8307a4582342;p=helm.git

diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma
index cd372394b..0e3be3a8f 100644
--- a/helm/software/matita/library/list/in.ma
+++ b/helm/software/matita/library/list/in.ma
@@ -113,8 +113,7 @@ intros 5.elim l
   [elim (not_in_list_nil ? ? H1)
   |elim H2
     [simplify;rewrite > H;reflexivity
-    |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;rewrite > H5;
-     reflexivity]].
+    |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;reflexivity]].
 qed.
 
 lemma in_list_filter_to_p_true : \forall l,x,p.
@@ -146,7 +145,7 @@ intros 3;elim l
   [elim (not_in_list_nil ? ? H)
   |elim (in_list_cons_case ? ? ? ? H1)
      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
-     |simplify;apply (bool_elim ? (p t));intro;rewrite > H4;simplify
+     |simplify;apply (bool_elim ? (p t));intro;simplify;
         [apply in_list_cons;apply H;assumption
         |apply H;assumption]]]
 qed.