xxx

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index f9346809bccc0509da6c995aae79ae422007ab09..15912d2645690cbd647c638173646e77d7884a8a 100644 (file)
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -4,14 +4,10 @@ for @{ 'exists ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
 
-axiom a : Type.
-
 notation "hvbox(a break \to b)" 
   right associative with precedence 20
 for @{ \forall $_:$a.$b }.
 
-axiom b : Type → Type.
-
 notation < "hvbox(a break \to b)" 
   right associative with precedence 20
 for @{ \Pi $_:$a.$b }.