At:
assert term eq
3
1.
a: Tree(ts())
2.
u: Tree(ts())
Type{i'}
3.
w: a:{v:Tree(ts())| u(v) }
b:Tree(ts()). term_eq(a;b) 
a = b
4.
y1: {v:Tree(ts())| u(v) }
5.
y2: {v:Tree(ts())| u(v) }
6.
b: Tree(ts())
7.
u1: Tree(ts())Type{i'}
8.
w1: b:{v:Tree(ts())| u1(v) }term_eq(tree_node( < y1, y2 > );b) tree_node( < y1, y2 > ) = b
9.
x: ts()
False tree_node( < y1, y2 > ) = tree_leaf(x)
By:
Auto
THEN
ApFunToHypEquands `z' Case(z) Case x;y = > 0 Default = > 1 
-1
THEN
Reduce -1
THEN
TreeInd -1
THEN
Reduce 0
Generated subgoals:
None
About:
