Is there a typo on page 25 of the OptComp notes, in the (COND) rule? If not could someone explain it to me... There's t on the top line of the rule, and t' on the bottom line - and no obvious way to link t and t' ? I seem to remember (from last term) that when doing proofs using it, t=t' usually works? So should the dash be there? I might e-mail Dr. Mycroft if no-one knows... Mond