AP_TERM : term -> thm -> thm
STRUCTURE
SYNOPSIS
Applies a function to both sides of an equational theorem.
DESCRIPTION
When applied to a term f and a theorem A |- x = y, the inference rule AP_TERM returns the theorem A |- f x = f y.
      A |- x = y
   ----------------  AP_TERM f
    A |- f x = f y

FAILURE
Fails unless the theorem is equational and the supplied term is a function whose domain type is the same as the type of both sides of the equation.
SEEALSO
HOL  Kananaskis-13