Hola.
Sobre lo primero, ponés "... yo lo pense como que los elementos que se agregan para las listas m y n pueden ser distintos y aun asi mantener el largo de la lista". Esto no es correcto. Las listas deberían ser iguales y en tal sentido la segunda opción es correcta. También podría ser que uses a y b pero deberías exigir que fueran iguales (eq a b), donde eq sería la relación de igualdad para elementos de tiipo A y en tal sentido debería ser un parámetro de eq_list.
Sobre lo segundo, está bien MemL. En relacción al forall, si se podría.
Saludos, Carlos