Nuprl - Proof: tree leaf one one 1 3

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: tree leaf one one 1 3

1. E : Type
2. x1 : E
3. x2 : E
4. tree_leaf(x1) = tree_leaf(x2)
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

By:

Reduce -1

Generated subgoals:

None

About:

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