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

None

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