At:
assert term eq
1
2
1
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.
x: ts()
5.
b: Tree(ts())
6.
u1: Tree(ts())Type{i'}
7.
w1: b:{v:Tree(ts())| u1(v) }term_eq(tree_leaf(x);b) tree_leaf(x) = b 
Tree(ts())
8.
x1: ts()
9.
tree_leaf(x) = tree_leaf(x1) Tree(ts())
10.
z: Tree(ts())
Case(z) Case tree_leaf(u) = > u Default = > x = Case(z) Case tree_leaf(u) = > u Default = > x ts()
By:
TreeInd -1
THEN
Reduce 0
Generated subgoals:
None
About:
