Is there a variant of apply which can discharge non-unifiable terms through equalities? E.g.,

old state:

x, z : nat ; H : forall y, P x 5 y |- P z 5 z

awesome_apply H.

new state:

x, z : nat ; H : P x |- x = z

I haven't seen it in Coq but I've written a similar one in Lean. I can help you write `awesome_apply`

. By the way, great naming there :)

SSReflect's `congr`

tactic does something like this

The file LibTactics.v distributed in Software Foundations defines a tactic called `applys_eq`

that does this kind of thing, but you must manually specify the variables that should give an equation. In your case, this would give `applys_eq H 1 3`

(the variables are counted from the right).

Last updated: Sep 28 2023 at 11:01 UTC