At: tc functionality 1
1. x: SimpleType
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
||r1|| = 2 & x 
term_types(ds1;da1;de;r1[0]) & x term_types(ds1;da1;de;r1[1])
||r1|| = 2 & x term_types(ds2;da2;de;r1[0]) & x term_types(ds2;da2;de;r1[1])
By:
Analyze 0
THEN
Analyze 0
THEN
Analyze -1
THEN
Analyze 0
THEN
Try Trivial
THEN
Try (RW (SweepDnC (HypC 8 ORELSEC HypC 9)) 0)
THEN
Try (RW (SweepDnC (HypC 8 ORELSEC HypC 9)) -2)
Generated subgoals:None
About:
