I think I actually proved a few substantial lemmas in LF+i 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...