It is not so difficult to conceive an appartness relation for Peano numbers. Its even possible to make a reified eq/3 predicate like here.
Question is now, whether we can push the boundary and also
implement Scheme equal? predicate in a pure and reified manner?
Problem would be for example to realize this reductions,
also known as δ-rule (see Chapter 6 Extensions here):
δxx ~~> T
δxy ~~> F if x and y are not identical
In case terms are represented with deBruijn indexes. This
would incorporate alpha conversion into the equal? predicate
besides handling lists (trees). Pure can mean intrinsically pure
or operational pure, as defined in the logical purity tag.
Test case is pure intersection with lists (trees), instead only Peano numbers.