Buenas,
Me está sucediendo lo siguiente y busco en google y tampoco logro entender qué está pasando.
Tengo de hipótesis
H1 : exists ys' : List X, ys = ys' ++' xs
y si hago elim H1 obtengo el error
Cannot find the elimination combinator ex_rec, the elimination of the inductive definition ex on sort Set is probably not allowed.
Y si hago destruct H1 as [ys' H1] obtengo
Case analysis on sort Set is not allowed for inductive definition ex.
Por si acaso lo que está en el goal es
xs << zsAlguna idea? Siento que estuve en esta misma situación un montón de veces ya. No veo qué tiene de diferente esta vez.
Saludos!