X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fbertrand.ma;h=17f4c72e0078ded8e054dc4e750e26aa6b876ea5;hb=6b61a9e6698a7c1936adf217b599e34e65a5e4c9;hp=7a0363a58117f7455ef7ed127ef339542c151369;hpb=2490d1bf464e276c581ca7b0b7956df2b0f7a490;p=helm.git

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index 7a0363a58..17f4c72e0 100644
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -42,10 +42,10 @@ let rec checker l \def
          | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
 
 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
-intros 2;simplify;intro;generalize in match H;elim l
+intros 2;simplify;intro;elim l in H ⊢ %
   [reflexivity
-  |change in H2 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
-   apply (andb_true_true ? ? H2)]
+  |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
+   apply (andb_true_true ? ? H1)]
 qed.
 
 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to