I am trying to figure out how to write something analogous to the first order unification done by apply and rewrite, for slightly different purposes.

I have a theorem of the form `\forall x, A x = B x`

and my goal is of the form `P(A(t))`

. I am trying to get hold of the equality `A(t) = B(t)`

that would come from specializing `x`

to `t`

.

Ideally I am looking for an approach that would still work even if the left hand side of the given equality only agrees with a subterm of the goal up to convertibility, not strict syntactic equality

Last updated: Jan 31 2023 at 14:03 UTC