Build the Nth constructor function for a
Church-encoded algebraic data type.
Unlike Scott, recursive fields are folded by
applying them to all case-handlers.

A type descriptor is a Scott list of constructor specs.
Each spec is a Scott list of fields.
Each field (λx.x) marks a recursive position.
In Haskell notation:
  data Bit  = O | I             is [[],[]]
  data Nat  = Z | S Nat         is [[],[⊤]]
  data Bin  = E | O Bin | I Bin is [[],[⊤],[⊤]]
  data Pair = A | B Pair Pair   is [[],[⊤,⊤]]
Nat encodes as:
  λc.λn.c(λc.λn.n,
    λc.λn.c(λc.λn.c(λx.x, λc.λn.n),
    λc.λn.n))

A Church value folds recursive fields by applying
them to all case-handlers:
  Nat Z:       λz.λs.z
  Nat S(S(Z)): λz.λs.s(s(z))

Index is a Scott nat:
  Z = λs.λz.z, S(n) = λs.λz.s(n)

---

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.n, λc.λn.n)), λs.λz.z)
= λa.λb.a

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.n, λc.λn.n)), λs.λz.s(λs.λz.z))
= λa.λb.b

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.n)), λs.λz.z)
= λa.λb.a

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.n)), λs.λz.s(λs.λz.z))
= λa.λb.λc.c(a(b, c))

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.n))), λs.λz.z)
= λa.λb.λc.a

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.n))), λs.λz.s(λs.λz.z))
= λa.λb.λc.λd.c(a(b, c, d))

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.c(λc.λn.c(λx.x, λc.λn.n), λc.λn.n))), λs.λz.s(λs.λz.s(λs.λz.z)))
= λa.λb.λc.λd.d(a(b, c, d))

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.c(λx.x, λc.λn.n)), λc.λn.n)), λs.λz.z)
= λa.λb.a

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.c(λx.x, λc.λn.n)), λc.λn.n)), λs.λz.s(λs.λz.z))
= λa.λb.λc.λd.d(a(c, d), b(c, d))

@main(λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.n, λc.λn.c(λc.λn.c(λx.x, λc.λn.c(λx.x, λc.λn.n)), λc.λn.n))), λs.λz.s(λs.λz.s(λs.λz.z)))
= λa.λb.λc.λd.λe.e(a(c, d, e), b(c, d, e))