Often in Coq I find myself doing the following: I have the proof goal, for example:
some_constructor a c d = some_constructor b c d
And I really only need to prove a = b
because everything else is identical anyway, so I do:
assert (a = b).
Then prove that subgoal, then
rewrite H.
reflexivity.
finishes the proof.
But it seems to just be unnecessary clutter to have those hanging around at the bottom of my proof.
Is there a general strategy in Coq for taking an equality of constructors and splitting it up into an equality of constructor parameters, kinda like a split
but for equalities rather than conjunctions.