Computation rule congruence rule

A rule performing an actual reduction step (e.g., Beta-reduction), as opposed to Congruence rule which merely propagate evaluation into subterms.