At: term types closed 2 2 2
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)
12. term_types(ds;da1;de;y2) = term_types(ds;da2;de;y2)
st_app(term_types(ds;da1;de;y1);term_types(ds;da1;de;y2)) = st_app(term_types(ds;da2;de;y1);...)
By:
RW (SweepDnC (FirstC (map HypC [-1;-2]))) 0
THEN
RelRST
Generated subgoals:None
About:
