Muitas vezes, em Coq, me pego fazendo o seguinte: tenho o objetivo de prova, por exemplo:

some_constructor a c d = some_constructor b c d

E eu realmente só preciso provara = b porque todo o resto é idêntico, então eu faço:

assert (a = b).

Então prove que subobjetivo, então

rewrite H.
reflexivity.

termina a prova.

Mas parece ser apenas uma desorganização desnecessária ter aqueles que estão por aí na parte inferior da minha prova.

Existe uma estratégia geral no Coq para obter uma igualdade de construtores e dividi-la em uma igualdade de parâmetros de construtores, como umsplit mas por igualdades em vez de conjunções.