]> matita.cs.unibo.it Git - helm.git/blob - test4.ma
4d7b03ce29cedd686540b379877b8b10ab74f2bb
[helm.git] / test4.ma
1 alias num (instance 0) = "natural number".
2 alias symbol "eq" (instance 0) = "leibnitz's equality".
3 theorem a:0=0.
4 reflexivity.