At:
member st app1
2
2
1.
s1: SimpleType
2.
s2: SimpleType
3.
s: SimpleType
4.
u: SimpleType
Type{i'}
5.
w: s1:{v:SimpleType| u(v) }s 
st_app1(s1;s2) 
st_eq(s1;s2s)
6.
y1: {v:SimpleType| u(v) }
7.
y2: {v:SimpleType| u(v) }
8.
st_eq(y1;s2)
s < > st_eq(tree_node( < y1, y2 > );tree_node( < s2, s > ))
By:
RecUnfold `st_eq` 0
THEN
Reduce 0
THEN
RWW "member_col_none" 0
THEN
RW assert_pushdownC 0
Generated subgoals:
None
About:
