Nuprl - Pf term_types

(9steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1. t: Term
2. u: TermType{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)

st_app(term_types(ds;da1;de;y1);term_types(ds;da1;de;y2)) = st_app(term_types(ds;da2;de;y1);...)

By: (InstHyp [y1;ds;da1;da2;de] 3) THENA (Try (Complete Auto))

Generated subgoals:

1 closed_term(y1)

2 11. term_types(ds;da1;de;y1) = term_types(ds;da2;de;y1)
st_app(term_types(ds;da1;de;y1);term_types(ds;da1;de;y2)) = st_app(term_types(ds;da2;de;y1);...)

About:

(9steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1	`closed_term(y1)`
2	11. `term_types(ds;da1;de;y1) = term_types(ds;da2;de;y1)` `st_app(term_types(ds;da1;de;y1);term_types(ds;da1;de;y2)) = st_app(term_types(ds;da2;de;y1);...)`