Def bif(b; bx.x(bx); by.y(by)) == if b x(*) else y(x.x) fi

is mentioned by

Thm* m,n:. nnsub(m;n)+1 = if mn then 0+1 else nnsub(m+1;n) fi	[sub_left_suc]
Thm* m,n,x:. nnsub(m;nnsub(n;x)) = if nx then m else nnsub(m+x;n) fi	[sub_left_sub]
Thm* m,n,x:. nnsub(m;n)+x = if mn then x else nnsub(m+x;n) fi	[sub_right_add]
Thm* m,n,x:. m+nnsub(n;x) = if nx then m else nnsub(m+n;x) fi	[sub_left_add]

In prior sections: hol bool hol num hol prim rec hol arithmetic 1

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