summaryrefslogtreecommitdiff
path: root/Precond.agda
AgeCommit message (Expand)Author
2012-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
2012-09-26rename suc-\== to suc-injectiveHelmut Grohne
2012-09-08give a sufficient precondition for theorem-2Helmut Grohne