X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fcantor.ma;h=754ef24b48eaa0c7ac6f90e4f5b89ab5734dd8df;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=3294017d789360859f4d6fe639b7eaea2ec8930e;hpb=13f687d1d7cc07a19dcf28e1624f78a3a9d9c840;p=helm.git

diff --git a/helm/software/matita/library/demo/cantor.ma b/helm/software/matita/library/demo/cantor.ma
index 3294017d7..754ef24b4 100644
--- a/helm/software/matita/library/demo/cantor.ma
+++ b/helm/software/matita/library/demo/cantor.ma
@@ -34,7 +34,7 @@ definition Z: Ω \sup axs ≝ {x | x ◃ emptyset}.
 theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z).
  intros 2; cases H; clear H;
  cut (a ◃ S' a);
-  [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); autobatch]]
+  [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); apply iter; autobatch]]
  cut (a ◃ emptyset);
   [2: apply transitivity; [apply (S' a)]
        [ assumption