Consider statement 3 of Lemma 9.3.1. Is there a context and type such that ? How about ? Explain your answers in detail.

9.3.1 LEMMA INVERSION OF THE TYPING RELATION 1. IfIx R, then x:R EI 2. If Ax:Ti. tz : R, then R T R2 for some R2 with I, x:Ti t R2 3. If r-tit2 : R, then there is some type T11 such that I-ti : T11-R and t2 : T11- 4. If I true R, then R Boo 5. If false R, then R Bool 6. IfT+ if t then t2 else t3 : R, then lt t : Bool and it t2, t3 : R Proof: Immediate from the definition of the typing relation. 9.3.1 LEMMA INVERSION OF THE TYPING RELATION 1. IfIx R, then x:R EI 2. If Ax:Ti. tz : R, then R T R2 for some R2 with I, x:Ti t R2 3. If r-tit2 : R, then there is some type T11 such that I-ti : T11-R and t2 : T11- 4. If I true R, then R Boo 5. If false R, then R Bool 6. IfT+ if t then t2 else t3 : R, then lt t : Bool and it t2, t3 : R Proof: Immediate from the definition of the typing relation