En la última parte, cuando pide generalizar las funciones, necesito, dados dos elementos de tipo A, saber si son iguales.
Para esto, me definí:
Parameter beq_gen : forall A:Set, A -> A -> bool.
Y luego:
Fixpoint memberGen (A : Set)(a : A)(l : list A) : bool :=
match l with
nilList => false
| cons a' l' => match (beq_gen A a a') with
true => true
| false => memberGen A a l'
end
end.
El tema es que haciéndolo así, no se podría hacer ninguna prueba basándose en memberGen porque faltaría definir la función beq_gen.
¿Cómo se puede hacer?
Saludos
P.D: Lo que sí funcionaría, y quizás tenga sentido, sería que memberGen reciba como parámetro la función de igualdad entre elementos de A.