From 7ae372991c6e02595c80bd4faaf437d39a965ce1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Oct 2009 14:46:19 +0000 Subject: [PATCH] instance fixed --- helm/software/matita/nlibrary/topology/igft.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 06c492e86..d6043fba2 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1168,7 +1168,7 @@ We now proceed with the proof of the infinity rule. D*) -alias symbol "covers" = "new covers set". +alias symbol "covers" (instance 3) = "new covers set". ntheorem new_coverage_infinity: ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U. #A; #U; #a; (** screenshot "n-cov-inf-1". *) -- 2.39.2