At:
member st app1
1
1
1.
s1: Tree(Label+Unit)
2.
s2: SimpleType
3.
s: SimpleType
4.
u: Tree(Label+Unit)
Type{i'}
5.
w: s1:{v:Tree(Label+Unit)| u(v) }s 
st_app1(s1;s2) 
st_eq(s1;s2s)
6.
x: Label+Unit
False st_eq(tree_leaf(x);tree_node( < s2, s > ))
By:
RecUnfold `st_eq` 0
THEN
Reduce 0
Generated subgoals:
None
About:
