Stream: Coq users

Topic: ✔ Show that (false -> Q) holds?

view this post on Zulip Jiahong Lee (Jun 07 2022 at 06:25):

Thanks, discriminate does the job for me. My updated solution:

Theorem andb_true_elim2'' : forall b c : bool,
  andb b c = true -> c = true.
  intros [].
  - simpl andb.
    intros c H.
    apply H.
  - discriminate.

As for easy and now, they are too much magic for me right now. So, I'll leave them for future usage.

view this post on Zulip Notification Bot (Jun 07 2022 at 06:28):

Jiahong Lee has marked this topic as resolved.

Last updated: Feb 08 2023 at 23:03 UTC