Hi! I'm using Eisbach's
match to perform a top-level pattern matching on a conclusion and pass part of the match result to a lower level tactic which _also_ performs pattern matching to identify suitable simplification operations. The initial conclusion has schematic variables, but they seem to have been lost by the time the low-level tactic is invoked. Does
match remove schematics?
Last updated: Dec 07 2023 at 08:19 UTC