Properties of well-formed factories

Key theorems: LFuncWF.toSig and FactoryWF.toSig (well-formed functions and factories have well-formed type signatures).

theorem Lambda.LFuncWF.toSig {T : LExprParams} {f : LFunc T} (h : LFuncWF f) : LFuncSigWF f

A well-formed function has a well-formed type signature.

theorem Lambda.FactoryWF.toSig {T : LExprParams} {fac : Factory T} (h : FactoryWF fac) : FactorySigWF fac

Every function of a well-formed factory has a well-formed type signature.