(9steps 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 subtype2 1 2
1. E : Type
2. y : Tree(E)Tree(E)
  inr(y)  rec(T.tree_con(E;T))
By: Analyze -1

Generated subgoal:

1 2. y1 : Tree(E)
3. y2 : Tree(E)
  inr(<y1,y2>)  rec(T.tree_con(E;T))
4 steps

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

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