At: tc closed rel 1 1
1. x: SimpleType
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_eq(x), r1))
8. ||r1|| = 2
9. x 
term_types(ds;da1;de;r1[0])
10. x term_types(ds;da1;de;r1[1])
11. 
i:
. closed_rel(mk_rel(relname_eq(x), r1)) 
i < ||r1|| closed_term(r1[i])
x term_types(ds;da2;de;r1[0])
By: ((InstHyp [0] -1) THEN (Assert term_types(ds;da2;de;r1[0]) = term_types(ds;da1;de;r1[0])))
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 subgoals:None
About:
