At:
term primed vars term vars
2
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.
y1: {v:Term| u1(v) }
6.
y2: {v:Term| u1(v) }
7.
(x term_primed_vars(y1)) 
(x term_primed_vars(y2))
(x term_vars(y1)) (x term_vars(y2))
By:
ParallelOp -1
THEN
EasyHyp
Generated subgoals:
None
About:
