[Agda] An Agda proof of the Church-Rosser theorem

[roconnor at theorem.ca]

URL: http://hub.darcs.net/roconnor/STLC/browse

This is my first development in Agda. I'm interested in getting some feedback on this work of any sort, including but not limited to

  * Abstractions in the standard library that I could take advantage of.
  * Standard naming conventions I should be using.
  * Where I should or shouldn't be using implicit arguments.
  * Better use of unicode operators.
  * Better argument orders.
  * Should I be using equational reasoning?
  * Ideas on how to use recursion schemes to simplify functions taking Terms. Recursions schemes for dependent families are kinda tricky.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''