g:Label, t:Term. term_mentions_guard(g;t) 
mentions_trace(t)
x.false
;x.false;x.false;x.false;x.x =
g;x,y. x 
y;t)
is mentioned by
| Thm* g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t) | [mentions_guard_mentions_trace] |
Try larger context:
GenAutomata