The mu tac builtin 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" e_{2} e_{3} "mu tac"
This example applies the mu tac builtin tactic to definite description expressions e_{2} and e_{3}.