uh not sure if irc gets images, here: nthFront :: ∀n :: Nat. ∀Ss :: Vector n Type. ∀T, U :: Type. (Ss B T → U) → T → Ss B U nthFront [] f = f nthFront (S : Ss) f t s = nthFront Ss (f s) t