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

is mentioned by

Thm* T:Type, i:, j:{i...}, k:{j...}, a:[T]Array{i..j}, b:[T]Array{j..k}. Thm* a @ b  [T]Array{i..k}	[array_append_wf]
Thm* T:Type, i:, j:{i...}, a:[T]Array{i..j}, m:. Thm* a[++m]  [T]Array{i+m..j+m}	[array_shift_wf]
Thm* T:Type, i:, j:{i...}, a:[T]Array{i..j}, m:{i..j}, n:{m..j}. Thm* a[m..n]  [T]Array{m..n}	[array_seg_wf]
Thm* T:Type, a:[T]Array , i:{a.l..a.u}. a[i]  T	[array_el_wf]
Thm* T:Type, i:, j:{i...}, a:[T]Array{i..j}, k:{i..j}. a[k]  T	[array_el_wfp]
Thm* i:, j:{i...}, a:[T]Array{i..j}. a.l = i & a.u = j	[p_array_properties]
Thm* T:Type{i}, i:, j:{i...}. [T]Array{i..j}  Type{[i']}	[p_array_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