walker (Nov 05 2022 at 10:23): walker (Nov 05 2022 at 10:23):What is the mathcomp idiomatic way of doing remember (f x) as y ?
The reason is that I want to do induction over y.
What I don't like about remember (f x) as y is that it creates a proposition y = f x with automaticlly generated name that I cannot control.
Ana de Almeida Borges (Nov 05 2022 at 11:57):move eqfxy: (f x) => y.
Notification Bot (Nov 05 2022 at 13:09):walker has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC