now. Good, good.
It looks as if I might actually get in on a paper about this.
Should read over the revised Canonical Forms et alia paper.
Also Frank gave me something by Gougen that does things
semantically --- I don't really understand it very well yet.
Honestly, I think I would feel better about a syntactic
proof of `structural' things like functionality, and I'm
fairly optimistic about them going through without adding
too much to the system that might fuck up adequacy of algorithmic
equality. Then again, maybe my intuition for these things
isn't very well-fueled by experience...
