At: tc functionality 2
1. y: Label
2. r1: Term List
3. ds1: Collection(dec())
4. ds2: Collection(dec())
5. da1: Collection(SimpleType)
6. da2: Collection(SimpleType)
7. de: sig()
8. ds1 = ds2
9. da1 = da2
||de.rel(y)|| = ||r1|| 
& (
i:. i < ||r1|| 
(de.rel(y))[i] term_types(ds1;da1;de;r1[i]))
||de.rel(y)|| = ||r1|| & (i:. i < ||r1|| (de.rel(y))[i] term_types(ds2;da2;de;r1[i]))
By:
Analyze 0
THEN
Analyze 0
THEN
Analyze -1
THEN
Analyze 0
THEN
Try Trivial
THEN
UnivCD
THEN
InstHyp [i] -4
THEN
Try (RW (SweepDnC (HypC 8 ORELSEC HypC 9)) 0)
THEN
Try (RW (SweepDnC (HypC 8 ORELSEC HypC 9)) -1)
Generated subgoals:None
About:
