The appropriate side of the theorem is matched to the target subterm and the format of the theorem is matched to the format of the embedded instance; these matches have to be consistent with one another. If everything works, the target term is replaced with the appropriate instance of the other side of the theorem. New variables may be introduced by this process; such variables have automatically generated numerical suffixes to reduce the chance of unintended identifications of new variables with old ones or other new ones. The command initializecounter reinitializes the counter which provides the automatically generated numerals.
To enforce some degree of confluence, terms containing rule infixes or delay operators do not match anything for purposes of theorem application.
It should also be noted that the tactic interpreters are not applied to terms representing embedded theorems.