Buenas, estamos teniendo un problema con esta prueba, nos trancamos en una parte ya que aplicar inversion H no tiene ningún beneficio. La idea que aplicamos fue hacer induction en l1.
Definimos lo que hay que probar como:
Theorem ej16: forall (a:A) (l1 l2:list A), Mem A a l1 -> Mem A a (append A l1 l2).
Tenemos las siguientes hipótesis:
IHl1 : forall l2 : list A, Mem A a l1 -> Mem A a (append A l1 l2)
H : Mem A a (cons A a0 l1)
______________________________________(1/1)
Mem A a (append A l1 l2)
Alguna sugerencia?
Gracias.