Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

Instantiate a telescope with a substitution. Might reorder the telescope. instantiateTel (Γ : Tel)(σ : Γ --> Γ) = Γσ~ Monadic only for debugging purposes.