]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/test3.ma
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
checked in new version of matita from svn
[helm.git] / helm / matita / tests / test3.ma
1 alias symbol "eq" (instance 0) = "leibnitz's equality".
2 theorem a:\forall x.x=x.
3 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
4 goal 5.
5 exact nat.
6 intro.
7 reflexivity.
8 qed.
Unnamed repository; edit this file 'description' to name the repository.