The package defun provides defunctionalization helpers, most importantly
type family DeFun.Core.App allowing to write higher-order type families.
The singletons package also has its own type family Apply,
but the machinery is tied to the Sing / singletons.
In particular, the Lam counterpart SLambda is specialized to Sing arguments.
The defun's Lam is however fully general, so you can use your own singletons
or (importantly) singleton-like arguments.
The package provides few defunctionalized functions, and their term-level
variants can be found in defun-bool and defun-sop packages,
which use SBool and NP data types from singletons-bool and sop-core
packages respectively.
