Buenas,
Haciendo algunos reemplazos en secuencia en este ejercicio. Se me generan múltiples sub-goals que son idénticas.
¿Hay alguna forma de "eliminar" las sub-goals repetidas?
Por ahora venia encadenando los replace con try reflexivity. Eso me elimina las que se prueban con reflexivity (la mayoría), además, podría encadenar con try symmetry; try apply... De esta manera pruebo todo (salvo 1 sub-goal) pero no parece una manera muy prolija, sin contar que symmetry modifica la única sub-goal que me debería quedar al final.
Saludos.