Fix issue with typing LF pis

The problem was that in the typing constraints generated for

   {x:A} B

the variable x was being assumed to have the type typeof(A) instead
of the type phi(A). Thus, for

   {x:nat} add x x x

it would type the x in the body (add x x x) in the typing context

   [nat:lftype, x:lftype]

rather than in

   [nat:lftype, x:lfobj]

because typeof(nat) = lftype vs. phi(nat) = lfobj.