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

At: rel subst2 tc 1 2 2 1 1
1. y: Label
2. r1: Term List
3. as: (LabelTerm) List
4. ds: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. ||de.rel(y)|| = ||r1||
8. i:. i < ||r1|| (de.rel(y))[i] term_types(ds;da;de;r1[i])
9. x:Label. (x rel_primed_vars( < inr(y),r1 > )) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))
10. ||de.rel(y)|| = ||r1||
11. i:
12. i < ||r1||
13. (de.rel(y))[i] term_types(ds;da;de;r1[i])

(de.rel(y))[i] term_types(ds;da;de;term_subst2(as;r1[i]))
By: BackThru Thm* t:Term, s:SimpleType, as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(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))
Generated subgoal:

114. x: Label
15. (x term_primed_vars(r1[i]))
16. t: SimpleType
17. mk_dec(x, t) ds
t term_types(ds;da;de;apply_alist(as;x;x))

About:
pairproductlistless_thaninrapplyequalimpliesall

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