From cbb17fc4b8fe935a576af81838f767fe138a2611 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 22 Sep 2008 11:30:58 +0000 Subject: [PATCH] fixed auto invocation --- helm/software/matita/library/decidable_kit/decidable.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma index c1a8d5816..3478ef628 100644 --- a/helm/software/matita/library/decidable_kit/decidable.ma +++ b/helm/software/matita/library/decidable_kit/decidable.ma @@ -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] +[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type] rewrite > (eqb_true_to_eq ? ? H1); autobatch |2:cases (b2pT ? ? (lebP ? ?) H); [ elim n; [reflexivity|assumption] -- 2.39.2