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

At: tc closed rel 1 3
1. y: Label
2. r1: Term List
3. ds: Collection(dec())
4. da1: Collection(SimpleType)
5. da2: Collection(SimpleType)
6. de: sig()
7. closed_rel(mk_rel(relname_other(y), r1))
8. ||de.rel(y)|| = ||r1||
9. i:. i < ||r1|| (de.rel(y))[i] term_types(ds;da1;de;r1[i])
10. i:. closed_rel(mk_rel(relname_other(y), r1)) i < ||r1|| closed_term(r1[i])
11. i:
12. i < ||r1||

(de.rel(y))[i] term_types(ds;da2;de;r1[i])
By: ((InstHyp [i] -3) THEN (Assert term_types(ds;da2;de;r1[i]) = term_types(ds;da1;de;r1[i]))) THENL [BackThru Thm* t:Term, ds:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(). closed_term(t) term_types(ds;da1;de;t) = term_types(ds;da2;de;t) ;RW (SweepDnC (HypC -1)) 0]
Generated subgoal:

113. closed_term(r1[i])
14. term_types(ds;da2;de;r1[i]) = term_types(ds;da1;de;r1[i])
(de.rel(y))[i] term_types(ds;da1;de;r1[i])

About:
listless_thanapplyequalimpliesall

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