eliminators are proof relevant eliminations.

From comment by Andrej Bauer

Eliminators are proof relevant eliminations.

From comment by Kevin Buzzard

A constructor for X is a way of making things of type X, and an eliminator for X is a way of using things of type X to make other stuff (i.e. a way to make functions from X to other types).