A menudo en Coq me encuentro haciendo lo siguiente: Tengo el objetivo de la prueba, por ejemplo:

some_constructor a c d = some_constructor b c d

Y realmente solo necesito demostrara = b porque todo lo demás es idéntico de todos modos, así que hago:

assert (a = b).

Entonces demuestre ese objetivo secundario, luego

rewrite H.
reflexivity.

Termina la prueba.

Pero parece ser un desorden innecesario tener a esos dando vueltas en el fondo de mi prueba.

¿Existe una estrategia general en Coq para tomar una igualdad de constructores y dividirla en una igualdad de parámetros de constructor, algo así como unsplit pero para igualdades en lugar de conjunciones.