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

At: term subst2 tc 1 2
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. x: Label
5. s: SimpleType
6. as: (LabelTerm) List
7. ds: Collection{i}(dec())
8. da: Collection{i}(SimpleType)
9. de: sig()
10. s dec_lookup(ds;x)
11. x@0:Label. (x@0 [x]) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))

s term_types(ds;da;de;apply_alist(as;x;x))
By:
BackThruSomeHyp
THEN
Try (RWW "member_singleton" 0)
THEN
AllHyps (RWW "member_dec_lookup")
Generated subgoals:

None

About:
productlistconsnilsetapplyfunctionuniverseimpliesall

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