Hola Eliana.
Si, es correcto hacer lo que decís.
Otra alternativa es declarar antes (por ejemplo al inicio de la sección de este ejercicio):
Variable A : Set.
En este caso el parámetro del Set en MemL podría ser omitido; así:
Variable A: Set.
Inductive MemL (a : A) : list A -> Prop :=
| here : forall l : list A, MemL a (cons a l)
| there : forall l : list A, MemL a l -> forall b : A, MemL a (cons b l).
Al cerrar luego la sección del ejercicio, Coq generaliza las definiciones considerando las variables definidas (que son globales a la sección).
Pueden elegir la opción que prefieran, ya que a partir del práctico 4 no hay plantillas predefinidas.
Saludos, Carlos