some TS work for lambda p and slight cleanup of current translation proof.