At:
closed term mng1
1.
t: Term
2.
u: TermType{i'}
3.
w: t:{v:Term| u(v) }e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)
4.
x: Label
5.
e: Top
6.
s: Top
7.
a1: Top
8.
a2: Top
9.
tr: Top
10.
closed_term(x)
a1 ~ a2
By:
Unfold `closed_term` -1
THEN
Unfold `term_free_vars` -1
THEN
Reduce -1
THEN
SimpHyp -1
Generated subgoals:
Type{i'}
e,s,a1,a2,tr:Top. closed_term(t) 
([[t]] e s a1 tr ~ [[t]] e s a2 tr)
a1 ~ a2