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

is mentioned by

Thm* x,y:A, P:(AProp), i,j:. Thm* P(if i=j x else y fi)  P(if i=j x else y fi)	[eq_int_cases_test]
Thm* i,j:. (i=j) = true  i = j	[eq_int_eq_true_elim]
Thm* i,j:. (i=j) = false  i  j	[eq_int_eq_false_elim]
Thm* i,j:. i = j  (i=j) = true	[eq_int_eq_true]
Thm* i,j:. i  j  (i=j) = false	[eq_int_eq_false]
Thm* f:(ST), b:, p,q:S. f(if b p else q fi) = if b f(p) else f(q) fi	[fun_thru_ite]
Thm* b:, x,y:T. b  if b x else y fi = x	[ite_rw_true]
Thm* b:, x,y:T. b  if b x else y fi = y	[ite_rw_false]
Thm* n:, i:{1..n}. 0 = 0 & n = 0  False	[ite_rw_test]
Thm* x,y:. xy  xy	[assert_of_le_int]
Thm* p,q:. pq  (p  q)	[assert_of_bimplies]
Thm* p,q:. (p  q)  p  q	[assert_of_bor]
Thm* p,q:. (pq)  p & q	[assert_of_band]
Thm* p:. p  p	[assert_of_bnot]
Thm* p,q:. p=q  p = q	[assert_of_eq_bool]
Thm* x,y:. x=y  x = y	[assert_of_eq_int_rw]
Thm* x,y:. x<y  x<y	[assert_of_lt_int]
Thm* x,y:Atom. x=yAtom  x  y	[neg_assert_of_eq_atom]
Thm* x,y:. x=y  x  y	[neg_assert_of_eq_int]
Thm* x,y:. x=y  x = y	[assert_of_eq_int]
Thm* x,y:Atom. x=yAtom  x = y	[assert_of_eq_atom]
Thm* a,b:. (a  b)  a = b	[iff_imp_equal_bool]
Thm* b:. Dec(b)	[decidable__assert]
Thm* b:. b = false  b	[eqff_to_assert]
Thm* b:. b = true  b	[eqtt_to_assert]
Thm* b:. b  b = false	[not_assert_elim]
Thm* b:. b  b = true	[assert_elim]
Thm* u:. (utrue) = u	[band_tt_simp]
Thm* u:. (ufalse) = false	[band_ff_simp]
Thm* u:. (u  true) = true	[bor_tt_simp]
Thm* u:. (u  false) = u	[bor_ff_simp]
Thm* u,v:. uv  u  v	[assert_functionality_wrt_bimplies]
Thm* u,v,w:. uv  vw  uw	[bimplies_transitivity]
Thm* u,v:. u = v  uv	[bimplies_weakening]
Thm* i,j:. ij = (j<i)	[bnot_of_le_int]
Thm* p,q:. (p  q) = (pq)	[bnot_thru_bor]
Thm* p,q:. (pq) = (p  q)	[bnot_thru_band]
Thm* p:. p = p	[bnot_bnot_elim]
Thm* a,b:. Dec(a = b)	[decidable__equal_bool]
Thm* P:(Prop). P(false)  P(true)  (b:. P(b))	[bool_ind]
Thm* b:. b = true  b = false	[bool_cases]
Thm* b:. 0b2i(b) & b2i(b)1	[b2i_bounds]
Thm* b:, A:Type, p,q:A. if b p else q fi  A	[ifthenelse_wf]

In prior sections: core well fnd int 1

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