unbreak lots more stuff
fill in lots of missing proofs
update to new coq-categories, base ND_Relation on inert sequences
lots of cleanup
use WeakFunctorCategory to prove GArrow/Reification isomorphism
re-arrange NaturalDeduction
use apply tactic in ReificationFromGeneralizedArrow; not sure why this is required
add HaskXXXXCategory, generalized arrows, and reifications