A type of well-founded trees of the form \(\W x {:} A. B\) was introduced in Martin-Löf 1982 (and in a more restricted form by Scott 1970). Elements of \(\W x {:} A. B\) are trees of varying and arbitrary branching: varying, because the branching type \(B\) is indexed by \(x {:} A\) and arbitrary because \(B\) can be arbitrary. The type is given by a generalized inductive definition since the well-founded trees may be infinitely branching. We can think of \(\W x{:}A. B\) as the free term algebra, where each \(a {:} A\) represents a term constructor \(\sup\,a\) with (possibly infinite) arity \(B[x := a]\).