Def Dec(P) == P  P

is mentioned by

Thm* E:(TTProp).  Thm* (EquivRel x,y:T. E(x,y)) Thm*  Thm* (x,y:T. Dec(E(x,y)))  (u,v:x,y:T//E(x,y). Dec(u = v))	[decidable__quotient_equal]
Thm* E:(TTProp).  Thm* (x,y:T. Dec(E(x,y)))  (f:(TT). x,y:T. (x f y)  E(x,y))	[dec_iff_ex_bvfun]

In prior sections: core int 1 bool 1 rel 1

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