t:Term, ds:Collection(dec()), da1,da2:Collection(SimpleType)
, de:sig(). closed_term(t) 
term_types(ds;da1;de;t) = term_types(ds;da2;de;t)t1,t2:Term. closed_term(t1 t2) 
closed_term(t1) & closed_term(t2)| Theorem | Name |
|
Thm* t:Term, ds:Collection(dec()), da1,da2:Collection(SimpleType)
, de:sig(). closed_term(t) term_types(ds;da1;de;t) = term_types(ds;da2;de;t) | [term_types_closed] |
| cites | |
|
Thm* t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2) | [closed_tapp] |