At:
mentions guard mentions trace
1
1.
g: Label
2.
t: Term
3.
u: Term
Type{i'}
4.
w: t:{v:Term| u(v) }term_mentions_guard(g;t) 
mentions_trace(t)
5.
y1: {v:Term| u(v) }
6.
y2: {v:Term| u(v) }
7.
term_mentions_guard(g;y1) 
term_mentions_guard(g;y2)
mentions_trace(y1) mentions_trace(y2)
By:
All (RW assert_pushdownC)
THEN
ParallelOp -1
THEN
EasyHyp
Generated subgoals:
None
About:
