fancybred, neelk, simrob, and carsten varming.I think I have very nearly figured out how to show correctness of focussing without any nasty commutativity lemmas. Frank even used the phrase "cool idea", although it was prefixed by the phrase "might be a", since it's still conditional on it all working out.
