MarkB
generic
Sections
NuprlLIB
Doc
Def
R preserves P ==
x,y:T. P(x)
(x R y)
P(y)
is mentioned
In prior sections:
mb
nat
MarkB
generic
Sections
NuprlLIB
Doc
x,y:T. P(x) 
(x R y) P(y)