Wesley Phoa's Intro on Fibrations, Toposes, Effective Toposes

Hello, Questions concerning: http://www.lfcs.informatics.ed.ac.uk/reports/92/ECS-LFCS-92-208/ I am familiar with natural deduction and sequents. In the chapter on Toposes (Chapter 3), I have some questions about the very beginning where propositional calculus (intuitionistic) is discussed 1) Did he leave out the Elimination rule for V? I do see in the second line on far right a rule for V, but it doesn't look like EV??? 2) I don't understand the Structual rules. Can anybody give me a short explanation? Regards, Bill Halchin