Congruence Closure in Intensional Type Theory