[CST-2] Types: y2000p9q13

[David Singleton]

Has anyone done this question, and could they tell me how to do the
proof?

I presume that we need to show that if phi holds of a judgement,
phi still holds when the axiom and rules are applied.

I think I've managed this for the axiom.

How do we proceed - if by structural induction, on what?

I tried substituting the rules into each \Phi (since \Phi
holds of judgements and the rules hold of the judgements),
but this didn't seem to get me anywhere.

Thanks,

David

-- 
David Singleton    _________________      St John's College, Cambridge
 C5 3rd Crt        +44(0)7980 641608   http://www.srcf.ucam.org/~dps29