1. E : Type
2. x1 : E
3. x2 : E
4. tree_leaf(x1) = tree_leaf(x2)
  x1 = x2

By:	ApFunToHypEquands `z' if is_leaf(z) leaf_value(z) else x1 fi E -1

1	5. z : Tree(E)   if is_leaf(z) leaf_value(z) else x1 fi   =   if is_leaf(z) leaf_value(z) else x1 fi	1 step
2	Tree(E) = Tree(E)	Auto
3	5. if is_leaf(tree_leaf(x1)) leaf_value(tree_leaf(x1)) else x1 fi 5. = 5. if is_leaf(tree_leaf(x2)) leaf_value(tree_leaf(x2)) else x1 fi   x1 = x2	1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html