fact: Definition with_component {ix j α} (initializer : impure ix unit) (c : component j ix) (finalizer : impure ix unit) (p : impure (ix + j) α) : impure ix α := initializer;; let* res := with_component_aux c p in finalizer;; pure res.
imports: ExtLib(StateMonad)