Def P  Q == PQ

is mentioned by

Thm* x1,x2:E. tree_leaf(x1) = tree_leaf(x2)  Tree(E)  x1 = x2	[tree_leaf_one_one]
Thm* E:Type, t:Tree(E). is_leaf(t)  leaf_value(t)  E	[leaf_value_wf]

In prior sections: core well fnd int 1 bool 1 sqequal 1 prog 1

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html