Stream: Coq users

Topic: ✔ destruct leaving a definition instead of an equality

view this post on Zulip Guillaume Melquiond (May 03 2024 at 13:04):

Isn't it just a matter of doing set (a' := a); destruct a; rename a' into a?

view this post on Zulip Michael Soegtrop (May 03 2024 at 13:56):

Thanks, this works! I didn't have the idea to destruct the right hand side of the definition.

view this post on Zulip Notification Bot (May 03 2024 at 13:56):

Michael Soegtrop has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC