(5steps total) PrintForm Definitions mb tree Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: tree leaf one one
  E:Type, x1,x2:E. tree_leaf(x1) = tree_leaf(x2)  Tree(E)  x1 = x2
By: Auto

Generated subgoal:

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

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

(5steps total) PrintForm Definitions mb tree Sections MarkB generic Doc