Def  i=j == if i=j true ; false fi

is mentioned by

Thm*  f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y)	[nsub_bij_least_preimage_inverse]
Thm*  f:(a onto b). (y.least x:. f(x)=y)  b inj a	[nsub_surj_imp_a_rev_inj]
Thm*  (A+B) ~ (i:2if i=0 A else B fi)	[card_union_vs_sigma]
Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)	[union_sigma_inverses]
Thm*  A,B:Type. sigma_to_union  (i:2if i=0 A else B fi)(A+B)	[sigma_to_union_wf]
Thm*  A,B:Type. union_to_sigma  (A+B)(i:2if i=0 A else B fi)	[union_to_sigma_wf]
Thm*  Dec(P)  (!i:2. if i=0 P else P fi)	[decidable_vs_unique_nsub2]
Thm*  f:(a onto b), y:b. f(least x:. f(x)=y) = y	[nsub_surj_least_preimage_works]
Thm*  f:(a onto b), y:b. (least x:. f(x)=y)  a	[nsub_surj_least_preimage_total]
Thm*  a:, b:, j:b, f:((a-1) inj {x:b| x = j }). Thm*  (i.if i=a-1 j else f(i) fi)  a inj b	[nsub_inj_fill_typing]
Thm*  IsEqFun(b;i,j. i=j)	[eq_int_is_eq_nsub]
Def  prev_nat_pair(xy) == xy/x,y. if x=0 <y-1,0> else <x-1,y+1> fi	[prev_nat_pair]
Def  next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else <x+1,y-1> fi	[next_nat_pair]
Def  [x/ xs](i) == if i=0 x else xs(i-1) fi	[seq_cons]
Def  sigma_to_union(e) == e/i,u. if i=0 inl(u) else inr(u) fi	[sigma_to_union]
Def  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)	[compose_iter]
Def  Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f	[delete_fenum_value]

In prior sections: bool 1 LogicSupplement int 2 num thy 1

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