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

At: rel subst tc 1 2
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_vars( < inr(y),r1 > )) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))

||de.rel(y)|| = ||map(t.term_subst(as;t);r1)|| & (i:. i < ||map(t.term_subst(as;t);r1)|| (de.rel(y))[i] term_types(ds;da;de;map(t.term_subst(as;t);r1)[i]))
By: Analyze 0
Generated subgoals:

1 ||de.rel(y)|| = ||map(t.term_subst(as;t);r1)||
210. ||de.rel(y)|| = ||map(t.term_subst(as;t);r1)||
i:. i < ||map(t.term_subst(as;t);r1)|| (de.rel(y))[i] term_types(ds;da;de;map(t.term_subst(as;t);r1)[i])

About:
pairproductlistless_thaninrlambdaapplyequalimpliesall

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