updated the definition of theta and gamma in type judgment and some typing rules