made executable again

[helm.git] / helm / software / matita / library / demo / cantor.ma

diff --git a/helm/software/matita/library/demo/cantor.ma b/helm/software/matita/library/demo/cantor.ma
index 3294017d789360859f4d6fe639b7eaea2ec8930e..754ef24b48eaa0c7ac6f90e4f5b89ab5734dd8df 100644 (file)
--- 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