lift package:Agda

Lift a computation from the argument monad to the constructed monad.
Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ
Restore TCState, do not touch CommandState.
Lift a TCM action transformer to a CommandM action transformer.
Ditto, but restore state.
Lift a computation in the Parser monad to the LookAhead monad.
Lift a substitution under k binders.