(2steps 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 wf
  E:Type. Tree(E)  Type
By: UnivCD THEN Unfold `tree` 0 THEN Unfold `member` 0

Generated subgoal:

1 1. E : Type
  rec(T.tree_con(E;T)) = rec(T.tree_con(E;T))
1 step

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

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