At: term types closed 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. term_free_vars(x) = nil
da1 = da2
By:
Unfold `term_free_vars` -1
THEN
Reduce -1
Generated subgoal:| 1 | 9. [x] = nil
da1 = da2 |
About:
