s1,s2:SimpleType. st_eq(s1;s2) s1 = s2

1

1. s1: SimpleType 2. u: SimpleTypeType{i'} 3. w: s1:{v:SimpleType| u(v) }s2:SimpleType. st_eq(s1;s2) s1 = s2 4. x: Label+Unit 5. s2: SimpleType 6. u1: SimpleTypeType{i'} 7. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_leaf(x);s2) tree_leaf(x) = s2 8. x1: Label+Unit 9. InjCase(x; x'. InjCase(x1; y'. x' = y'; b. false); a. InjCase(x1; y'. false; b. true)) tree_leaf(x) = tree_leaf(x1) SimpleType

2

1. s1: SimpleType 2. u: SimpleTypeType{i'} 3. w: s1:{v:SimpleType| u(v) }s2:SimpleType. st_eq(s1;s2) s1 = s2 4. y1: {v:SimpleType| u(v) } 5. y2: {v:SimpleType| u(v) } 6. s2: SimpleType 7. u1: SimpleTypeType{i'} 8. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_node( < y1, y2 > );s2) tree_node( < y1, y2 > ) = s2 9. y3: {v:SimpleType| u1(v) } 10. y4: {v:SimpleType| u1(v) } 11. st_eq(y1;y3)st_eq(y2;y4) tree_node( < y1, y2 > ) = tree_node( < y3, y4 > ) SimpleType

About: