1 | 9. g:Label.
term_mentions_guard(g;r.args[i])

(( [[ < d daa | te(g,d.lbl) > ]] rho) List) (rho(lbl_pr( < Trace, g > ))) 10. ||map( t.term_subst(as;t);r.args)|| = ||r.args||  11. g: Label 12. term_mentions_guard(g;map( t.term_subst(as;t);r.args)[i]) 13. x,y:Term. x = y  (x ~ y) map( t.term_subst(as;t);r.args)[i] = term_subst(as;r.args[i]) |