The first group of inference rules are general rules including rules of assumption, substitution, and context formation. There are also rules which express that equalities are equivalence relations. There are numerous such rules, and we only show the particularly important rule of type equality which is crucial for computation in types: