(5steps total) PrintForm Definitions mb tree Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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