Make typing lemmas about continuations and functions easier to apply.

By letting them only speak about lits in their conclusions, and use [length] as the length parameter of vec. Also simplified substitutions of vectors.