From b6dde94d890e89aaaf4e0c2ac84e79bcb617e81f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 14:49:00 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/topology/cantor.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma index 7864a1ea6..bd8a04a22 100644 --- a/helm/software/matita/nlibrary/topology/cantor.ma +++ b/helm/software/matita/nlibrary/topology/cantor.ma @@ -87,8 +87,8 @@ ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z. *; #a; *; #ZSa; #SaZ; ncut (a ◃ Z); ##[ nlapply (axiom_cond … a one); #AxCon; nchange in AxCon with (a ◃ S a); - (* nauto; *) napply (cover_monotone … AxCon); nassumption; ##] #H; -ncut (a ◃ ∅); ##[ napply (transitivity … H); #x; #E; napply E; ##] #H1; + napply (cover_monotone … AxCon); nassumption; ##] #H; +ncut (a ◃ ∅); ##[ napply (transitivity … H); nwhd in match Z; nauto; ##] #H1; ncut (¬ a ∈ S a); ##[ napply (col2_4 … H1); ##] #H2; ncut (a ∈ S a); ##[ napply ZSa; napply H1; ##] #H3; nauto; -- 2.39.2