Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* a,b,c:. a *q b +q c =q a *q b +q a *q c	[qmul_dist_over_qadd]
Thm* p,q:. p *q q =q q *q p	[qmul_com]
Thm* p,q:. p +q q =q q +q p	[qadd_com]
Thm* p,q,r:. p +q q +q r =q p +q q +q r	[qadd_assoc]
Thm* p,q,r:. p *q q *q r =q p *q q *q r	[qmul_assoc]
Thm* p,q,r,s:. p =q q  r =q s  p *q r =q q *q s	[qmul_functionality]
Thm* p,q,r,s:. p =q q  r =q s  p +q r =q q +q s	[qadd_functionality]
Thm* x,y,z:. x =q y  y =q z  x =q z	[eq_rat_trans]
Thm* x,y:. x =q y  y =q x	[eq_rat_sym]
Thm* x:. x =q x	[eq_rat_refl]
Thm* p,q:. p *q q	[qmul_wf]
Thm* p,q:. p +q q	[qadd_wf]

In prior sections: core well fnd int 1 bool 1 int 2

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