At: term subst mentions guard 1 1 1
1. as: (Label
Term) List
2. g: Label
3. t: Term
4. u: Term
Type{i'}
5. w: t:{v:Term| u(v) }
subst_mentions_trace(as) 
term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t)
6. x1: Label
7. term_mentions_guard(g;apply_alist(as;x1;x1))
8. i: 
9. i < ||2of(unzip(as))||
10. apply_alist(as;x1;x1) = 2of(unzip(as))[i]
i < ||as||
By:
Unfold `unzip` -2
THEN
Reduce -2
THEN
RWO "map_length" -2
Generated subgoals:None
About:
