At: assert st eq 1 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: Unit
5. s2: SimpleType
6. u1: SimpleTypeType{i'}
7. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_leaf(inr(y1));s2) tree_leaf(inr(y1)) = s2
8. y: Unit
9. True
tree_leaf(inr(y1)) = tree_leaf(inr(y)) 
SimpleType
By:
Analyze 8
THEN
Analyze 4
THEN
Fold `it` 0
THEN
Fold `st_top` 0
Generated subgoals:None
About:
