Hanno Becker (Apr 16 2023 at 14:04): Hanno Becker (Apr 16 2023 at 14:04):Hi all. I have a pretty basic question and feel I'm missing the obvious: Which tactic would solve x = ?y but not f x = f ?y? A plain simp will do both, a plain clarsimp won't do either. I have to be cautious with premature instantiation of schematics, but where the goal is an equality of a schematic, instantiating it according to the equality seems safe and unavoidable to do.
Wolfgang Jeltsch (Apr 17 2023 at 15:21):Wild guess: (fact refl [of x]).
Last updated: Nov 13 2025 at 04:27 UTC