Nuprl - Pf term_subst2

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }s:SimpleType, as:(LabelTerm) List, ds:Collection{i}(dec()) , da:Collection{i}(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_primed_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst2(as;t))
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. s: SimpleType
7. as: (LabelTerm) List
8. ds: Collection{i}(dec())
9. da: Collection{i}(SimpleType)
10. de: sig()
11. a:SimpleType. a term_types(ds;da;de;y2) & as term_types(ds;da;de;y1)
12. x:Label. (x term_primed_vars(y1) @ term_primed_vars(y2)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))

a:SimpleType. a term_types(ds;da;de;term_subst2(as;y2)) & as term_types(ds;da;de;term_subst2(as;y1))

By: ExRepD THEN InstConcl [a] THEN Repeat BackThruSomeHyp THEN RWW "member_append" 0 THEN TrivialOr

Generated subgoals:

None

About:

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc