At:
closed term mng2
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.
y1: {v:Term| u(v) }
5.
y2: {v:Term| u(v) }
6.
e: Top
7.
s: Top
8.
a1: Top
9.
a2: Top
10.
tr: Top
11.
closed_term(y1 y2)
([[y1]] e s a1 tr([[y2]] e s a1 tr)) ~ ([[y1]] e s a2 tr([[y2]] e s a2 tr))
By:
RWW "closed_tapp" -1
THEN
Analyze
THEN
BackThruSomeHyp
Generated subgoals:
Type{i'}
e,s,a1,a2,tr:Top. closed_term(t) 
([[t]] e s a1 tr ~ [[t]] e s a2 tr)
([[y1]] e s a1 tr([[y2]] e s a1 tr)) ~ ([[y1]] e s a2 tr([[y2]] e s a2 tr))