Equality Definition

The equality function on is defined by primitive recursion as follows:

This is sometimes called syntactic identity, and is written as . Note that