X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Futil.ma;h=4f5e1542232f753e7fbb209ecc3fbb0a7ec69760;hb=194a530bca425408e72a6ea86afc2947b857da30;hp=41089172e56d6c76ece6e834aa665db4ba8feee9;hpb=68dcac85ab9510b2e3e272d964e3765cd116ddbb;p=helm.git

diff --git a/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/library/Fsub/util.ma
index 41089172e..4f5e15422 100644
--- a/helm/software/matita/library/Fsub/util.ma
+++ b/helm/software/matita/library/Fsub/util.ma
@@ -73,7 +73,7 @@ qed.
 
 lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t).
 intros;inversion H;intros
-  [destruct H2;left;symmetry;assumption
+  [destruct H2;left;symmetry;reflexivity
   |destruct H4;right;applyS H1]
 qed.
 
@@ -112,15 +112,12 @@ theorem append_to_or_in_list: \forall A:Type.\forall x:A.
 intros 3.
 elim l
   [right.apply H
-  |simplify in H1.inversion H1;intros
-    [destruct H3.left.rewrite < Hcut.
-     apply in_Base
-    |destruct H5.
-     elim (H l2)
-      [left.apply in_Skip.
-       rewrite < H4.assumption
-      |right.rewrite < H4.assumption
-      |rewrite > Hcut1.rewrite > H4.assumption
+  |simplify in H1.inversion H1;intros; destruct;
+    [left.apply in_Base
+    | elim (H l2)
+      [left.apply in_Skip. assumption
+      |right.assumption
+      |assumption
       ]
     ]
   ]