At:
term mng static u:Term, e,s,a,tr,tr':Top. mentions_trace(u) ([[u]] e s a tr' ~ [[u]] e s a tr)
By:
Analyze 0
THEN
TermInd 1
THEN
Reduce 0
THEN
UnivCD
THEN
Try (Complete Auto)
THEN
Try (SimpHyp -1)
THEN
Try (RW assert_pushdownC -1)
THEN
Try (Analyze THEN BackThruSomeHyp THEN (ParallelOp -1) THEN SimpConcl)
Generated subgoals:
u:Term, e,s,a,tr,tr':Top. 
mentions_trace(u) 
([[u]] e s a tr' ~ [[u]] e s a tr)