build explicit dictionary

Instead of building a proof object, the tactic builds a dictionary (that
contains the inj function).