(named "nightly builds" in the download page of Matita)
with a version strictly greater than 0.5.7.
-To read this tutorial in the HTML version, you need a decent browser
-equipped with a unicode capable font. Use the PDF version if some
-symbols are not correctly displayed.
+To read this tutorial in HTML format, you need a decent browser
+equipped with a unicode capable font. Use the PDF format if some
+symbols are not displayed correctly.
Orienteering
------------
D*)
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.