At: term types closed 2 2 1
1. t: Term
2. u: Term
Type{i'}
3. w: t:{v:Term| u(v) }
ds:Collection{i}(dec()), da1,da2:Collection{i}(SimpleType), de:sig().
closed_term(t) 
term_types(ds;da1;de;t) = term_types(ds;da2;de;t)
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. ds: Collection{i}(dec())
7. da1: Collection{i}(SimpleType)
8. da2: Collection{i}(SimpleType)
9. de: sig()
10. closed_term(y1 y2)
11. term_types(ds;da1;de;y1) = term_types(ds;da2;de;y1)
closed_term(y2)
By:
Inst
Thm* t1,t2:Term. closed_term(t1 t2) 
closed_term(t1) & closed_term(t2)
[y1;y2]
THEN
ThinTrivial
Generated subgoals:None
About:
