Still trying to figure out how to connect the proof I did to the way labelled deduction stuff is expressed in the literature. Trouble is I don't really understand the latter too well. I am too much exposed to the Frank-filtered version for it to be familiar.
In the evening went over to watch "Lost" with lincoln3. Only up to episode 9 and already so crazy.