# Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming Languages by Pierce on page 166. The term is $$t = (\lambda a:\mathrm{Ref}\mathrm{Bool}. \mathrm{if}\, \mathrm{true}\,\mathrm{then}\, !l_1\, !a\, \mathrm{else}\,0)\,\mathrm{ref}\,\mathrm{true}$$ where $$\mu(l_1)=\lambda x:\mathrm{Int}.x$$ So I need to find $$\Gamma, \Sigma,$$ and $$T$$ so that $$\Gamma\,|\,\Sigma\vdash t:T$$ I know you are supposed to show your work, but my problem is that $$t$$ doesn’t seem well-typed… What am I missing?