Derives forward and backward implication from equality of boolean terms.
DESCRIPTION
When applied to a theorem A |- t1 = t2, where t1 and t2 both have
type bool, the inference rule EQ_IMP_RULE returns the
theorems A |- t1 ==> t2 and A |- t2 ==> t1.
A |- t1 = t2
----------------------------------- EQ_IMP_RULE
A |- t1 ==> t2 A |- t2 ==> t1
FAILURE
Fails unless the conclusion of the given theorem is an equation between
boolean terms.