Häufig tue ich in Coq Folgendes: Ich habe das Beweisziel, zum Beispiel:

some_constructor a c d = some_constructor b c d

Und ich muss wirklich nur beweisen,a = b weil alles andere sowieso identisch ist, also mache ich:

assert (a = b).

Dann beweisen, dass Unterziel, dann

rewrite H.
reflexivity.

Beendet den Beweis.

Aber es scheint nur unnötige Unordnung zu sein, wenn die unten in meinem Beweis herumhängen.

ibt es in Coq eine allgemeine Strategie, wie man eine Gleichheit von Konstruktoren in eine Gleichheit von Konstruktorparametern aufteilt, so wie einsplit aber nicht für Konjunktionen, sondern für Gleichheiten.