Def  Dec(P) == P  P

is mentioned by

Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))	[card_split_decbl_squash]
Thm*  B:(AType), P:(AProp). Thm*  (i:A. Dec(P(i))) Thm*   Thm*  ((i:AB(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i))))	[card_split_sigma_dom_decbl]
Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))	[card_split_decbl]
Thm*  (x:A. Dec(P(x))) Thm*   Thm*  ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x))))	[card_split_prod_intseg_family_decbl]
Thm*  P:{P:(Prop)| i:. P(i) }.  Thm*  (i:. Dec(P(i)))  ({i:| P(i) & (j:. j<i  P(j)) })	[least_exists2]
Thm*  k:, P:{P:(kProp)| i:k. P(i) }. Thm*  (i:k. Dec(P(i)))  ({i:k| P(i) & (j:i. P(j)) })	[least_exists]
Thm*  Dec(P)  (!i:2. if i=0 P else P fi)	[decidable_vs_unique_nsub2]
Thm*  i,j:. Dec(i = j)	[decidable__nat_equal]

In prior sections: core int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 num thy 1 SimpleMulFacts

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