r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) tc(r;ds2;da2;de))

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])
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]))

About: