new implementation of the destruct tactic,

[helm.git] / matita / library / Fsub / util.ma

diff --git a/matita/library/Fsub/util.ma b/matita/library/Fsub/util.ma
index ac93f8ccf34d87a34db374802bcb18afe4ab2751..4f5e1542232f753e7fbb209ecc3fbb0a7ec69760 100644 (file)
--- a/matita/library/Fsub/util.ma
+++ b/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,23 +112,20 @@ 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
       ]
     ]
   ]
 qed.
 
 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
-      [ false \Rightarrow n
-      | true \Rightarrow m ].
+      [ true \Rightarrow n
+      | false \Rightarrow m ].
 intros;elim m;simplify;reflexivity;
 qed.