Patrick Nicodemus (Oct 19 2022 at 15:55): Patrick Nicodemus (Oct 19 2022 at 15:55):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: Apr 19 2024 at 04:02 UTC