At:
closed term mng22
1.
t: Term
2.
u: TermType{i'}
3.
w: t:{v:Term| u(v) }e,s,s',a1,a2,tr:Top. closed_term(t) ([[t]] e s s' a1 tr ~ [[t]] e s s' a2 tr)
4.
y1: {v:Term| u(v) }
5.
y2: {v:Term| u(v) }
6.
e: Top
7.
s: Top
8.
s': Top
9.
a1: Top
10.
a2: Top
11.
tr: Top
12.
closed_term(y1 y2)
([[y1]] e s s' a1 tr([[y2]] e s s' a1 tr)) ~ ([[y1]] e s s' a2 tr([[y2]] e s s' a2 tr))
By:
RWW "closed_tapp" -1
THEN
Analyze
THEN
BackThruSomeHyp
Generated subgoals:
Type{i'}
e,s,s',a1,a2,tr:Top. closed_term(t) 
([[t]] e s s' a1 tr ~ [[t]] e s s' a2 tr)
([[y1]] e s s' a1 tr([[y2]] e s s' a1 tr)) ~ ([[y1]] e s s' a2 tr([[y2]] e s s' a2 tr))