At:
term primed vars term vars
1
1.
x: Label
2.
u: Term
3.
u1: Term
Type{i'}
4.
w: u:{v:Term| u1(v) }(x 
term_primed_vars(u)) 
(x term_vars(u))
5.
x2: Label
6.
(x nil)
(x [x2])
By:
Unfold `l_member` -1
THEN
Reduce -1
THEN
ExRepD
Generated subgoals:
None
About:
