Stream: Coq users

Topic: ✔ need some help with a simpl proof


view this post on Zulip Notification Bot (Nov 09 2022 at 21:37):

yicx has marked this topic as resolved.

view this post on Zulip yicx (Nov 09 2022 at 21:37):

thank you, the idea that I can find some way other than induction is more than enough, have a wonderful day!

view this post on Zulip Pierre Castéran (Nov 10 2022 at 06:21):

yicx said:

thank you, the idea that I can find some way other than induction is more than enough, have a wonderful day!

To be precise, induction is massively used in the proof of lemmas L0 to L3.
It’s very usual, when stuck in an attempt to prove simply a property by induction, to prove (often by induction) a more general property.


Last updated: Feb 06 2023 at 12:04 UTC