Proves equality of equal functions applied to a term.
DESCRIPTION
When applied to a theorem A |- f = g and a term x, the inference
rule AP_THM returns the theorem A |- f x = g x.
A |- f = g
---------------- AP_THM (A |- f = g) x
A |- f x = g x
FAILURE
Fails unless the conclusion of the theorem is an equation, both sides
of which are functions whose domain type is the same as that of the
supplied term.