The mu tac built-in tactic applies a proof rule to definite description () expressions. The definite description expressions must be in antecedent or consequent predicates.
? 1 s true, p( s e) | 1 s true ? s p[e/( s e)]
? p( s e)
The proof rule is not applicable if there are any names in the schema s that refer to declarations that are in p but not in s.
"apply tactic" e2 e3 "mu tac"
This example applies the mu tac built-in tactic to definite description expressions e2 and e3.