same). The additional restriction of not allowing the elimination of a CProp
toward a Type makes the theory of Matita minimal in the following sense:
-<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="600px"/>
Theorems proved in CIC as implemented in Matita can be reused in a classical
and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
D*)
-
-alias symbol "exists" (instance 1) = "exists".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-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". *)