better description

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

diff --git a/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/library/Fsub/util.ma
index 582114c690a60afb840fa51b0eaaac2801c899ea..2e50ed5c014e581f70b89be131f48bf5dfef6fce 100644 (file)
--- a/helm/software/matita/library/Fsub/util.ma
+++ b/helm/software/matita/library/Fsub/util.ma
@@ -20,14 +20,14 @@ include "list/list.ma".
 (*** useful definitions and lemmas not really related to Fsub ***)
 
 lemma eqb_case : \forall x,y.(eqb x y) = true \lor (eqb x y) = false.
-intros;elim (eqb x y);auto;
+intros;elim (eqb x y);autobatch;
 qed.
        
 lemma eq_eqb_case : \forall x,y.((x = y) \land (eqb x y) = true) \lor
                                 ((x \neq y) \land (eqb x y) = false).
 intros;lapply (eqb_to_Prop x y);elim (eqb_case x y)
-  [rewrite > H in Hletin;simplify in Hletin;left;auto
-  |rewrite > H in Hletin;simplify in Hletin;right;auto]
+  [rewrite > H in Hletin;simplify in Hletin;left;autobatch
+  |rewrite > H in Hletin;simplify in Hletin;right;autobatch]
 qed.
 
 let rec max m n \def