An Extensible Equality Checking Algorithm for Dependent Type Theories