2 (* commento che va nell'ast, ma non viene contato
3 come step perche' non e' un executable
6 alias num (instance 0) = "natural number".
7 alias symbol "eq" (instance 0) = "leibnitz's equality".
16 apply cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1).
18 (* commenti che non devono essere colorati perche'
19 non c'e' nulla di eseguibile dopo di loro