At: assert st eq 1 1 2
1. s1: SimpleType
2. u: SimpleType
Type{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
By:
RW assert_pushdownC -1
THEN
Unfold `st` 0
THEN
Analyze
THEN
All (Fold `st`)
THEN
SmAuto
Generated subgoals:None
About:
