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
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