2of(unzip(as)))
i:
||as||. mentions_trace(2of(as[i])) i:||as||. mentions_trace(2of(as[i]))
Term) List
Type{i'}
subst_mentions_trace(as) 
term_mentions_guard(g;term_subst2(as;t)) term_mentions_guard(g;t) i:||as||. mentions_trace(2of(as[i]))
as:(LabelT) List, d:T, x:Label.
(apply_alist(as;x;d) 2of(unzip(as))) 
apply_alist(as;x;d) = d
[Term;as;x';x]
| 1 | 8. (apply_alist(as;x;x') 2of(unzip(as))) i:||as||. mentions_trace(2of(as[i])) |
| 2 | 8. apply_alist(as;x;x') = x' i:||as||. mentions_trace(2of(as[i])) |
About:
 |  |  |  |  |  |  |  |  |  |