Identity Elimination allows you to substitute in accord with an indentity in things you have already derived.
Preview shown for the Typed Forward Strict derivation type in the LRC_O system
