X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Fdecidable.ma;h=b2b21ccd26aa50e693b4b3e88cbe424076cc03a5;hb=73a66cce6e72c654fdcd0ce760c405a74af70d08;hp=3478ef628e44c5871298100c970e3f36c9b05370;hpb=cbb17fc4b8fe935a576af81838f767fe138a2611;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index 3478ef628..b2b21ccd2 100644
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -56,7 +56,7 @@ qed.
 
 lemma prove_reflect : ∀P:Prop.∀b:bool.
   (b = true → P) → (b = false → ¬P) → reflect P b.
-intros 2 (P b); cases b; intros; [left|right] autobatch.
+intros 2 (P b); cases b; intros; [left|right] [autobatch.|autobatch;]
 qed.   
   
 (* ### standard connectives/relations with reflection predicate ### *)
@@ -137,7 +137,7 @@ qed.
 
 lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
 intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type] 
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: (*autobatch type;*) apply lebW; assumption; ] 
    rewrite > (eqb_true_to_eq ? ? H1); autobatch
 |2:cases (b2pT ? ? (lebP ? ?) H); 
    [ elim n; [reflexivity|assumption]