Proof Method. rule_tac, erule_tac, drule_tac, frule_tac [isa-001A]
The typical rule, erule, drule, frule methods rely entirely on unification to determine how to instantiate the variables in the provided rule. Sometimes, it is useful to state explicitly how to instantiate some variables in the rule, particularly when dealing with quantifiers, or when there are multiple possible candidates.