Fixed the broken use of =cover=. Now I don't use it at all, actually.
Proved assr_lr==id, finally. Also added some stuff involving the twist arrow, and obtained the existence of terms app2 : mor ((B => C) * B) C cur2 : mor (A * B) C -> mor A (B => C) which satisfy the exact same equations from ccc.elf.
I fiddled with the higher-order stuff some more; I actually proved that a category equivalent to the terminal category exists - it takes like 30s to check the final declaration, and it spits out 3 pages of type information!. It's funny that the way I have things defined, categories are only determined up to equivalence. I supposed this is because of a lack of definition of object equality.