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