At: term types closed 1 1 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. x: Label
5. ds: Collection{i}(dec())
6. da1: Collection{i}(SimpleType)
7. da2: Collection{i}(SimpleType)
8. de: sig()
9. [x] = nil
da1 = da2
By: SimpHyp -1
Generated subgoals:None
About:
