The question asks to show that a statement fi(G,M,t) for a judgement G |- M : t is closed under the axioms and rules of the type system (PLC in this case). It's for 10 marks - I've tried doing it but it takes ages - is there a nice "clean" way of doing it in 10 minutes? Mat